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/aloul/FPGA_SAT05/normalized-fpga45_45_sat_pb.cnf.cr.opb
MD5SUM	da4cd22fd601b0d838453ba86be8f9aa
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	0
Optimality of the best value was proved	NO
Number of terms in the objective function	0
Biggest coefficient in the objective function	0
Number of bits for the biggest coefficient in the objective function	0
Sum of the numbers in the objective function	0
Number of bits of the sum of numbers in the objective function	0
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	46
Number of bits of the biggest sum of numbers	6
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	6.73997
Number of variables	3038
Total number of constraints	2160
Number of constraints which are clauses	2070
Number of constraints which are cardinality constraints (but not clauses)	90
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	22
Maximum length of a constraint	45
Trace number 5405

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-04-13 23:42:55 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3817 boxname=wulflinc15 idbench=57 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  da4cd22fd601b0d838453ba86be8f9aa  /oldhome/oroussel/tmp/wulflinc15/normalized-fpga45_45_sat_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc15/normalized-fpga45_45_sat_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc15/normalized-fpga45_45_sat_pb.cnf.cr.opb
IDLAUNCH: 3817
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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		: 450.999
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:        904176 kB
Buffers:         34976 kB
Cached:          73924 kB
SwapCached:       2144 kB
Active:          63572 kB
Inactive:        50348 kB
HighTotal:      131008 kB
HighFree:        53228 kB
LowTotal:       903652 kB
LowFree:        850948 kB
SwapTotal:     2097136 kB
SwapFree:      2094992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11068 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 00:02:58 (client local time) WITH STATUS 0 IN 1200.25 SECONDS
stats: 3817 7 1200.25 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2160 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ......................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[  89]---> BDD-cost:   87
c ---[  88]---> BDD-cost:   87
c ---[  87]---> BDD-cost:   87
c ---[  86]---> BDD-cost:   87
c ---[  85]---> BDD-cost:   87
c ---[  84]---> BDD-cost:   87
c ---[  83]---> BDD-cost:   87
c ---[  82]---> BDD-cost:   87
c ---[  81]---> BDD-cost:   87
c ---[  80]---> BDD-cost:   87
c ---[  79]---> BDD-cost:   87
c ---[  78]---> BDD-cost:   87
c ---[  77]---> BDD-cost:   87
c ---[  76]---> BDD-cost:   87
c ---[  75]---> BDD-cost:   87
c ---[  74]---> BDD-cost:   87
c ---[  73]---> BDD-cost:   87
c ---[  72]---> BDD-cost:   87
c ---[  71]---> BDD-cost:   87
c ---[  70]---> BDD-cost:   87
c ---[  69]---> BDD-cost:   87
c ---[  68]---> BDD-cost:   87
c ---[  67]---> BDD-cost:   87
c ---[  66]---> BDD-cost:   87
c ---[  65]---> BDD-cost:   87
c ---[  64]---> BDD-cost:   87
c ---[  63]---> BDD-cost:   87
c ---[  62]---> BDD-cost:   87
c ---[  61]---> BDD-cost:   87
c ---[  60]---> BDD-cost:   87
c ---[  59]---> BDD-cost:   87
c ---[  58]---> BDD-cost:   87
c ---[  57]---> BDD-cost:   87
c ---[  56]---> BDD-cost:   87
c ---[  55]---> BDD-cost:   87
c ---[  54]---> BDD-cost:   87
c ---[  53]---> BDD-cost:   87
c ---[  52]---> BDD-cost:   87
c ---[  51]---> BDD-cost:   87
c ---[  50]---> BDD-cost:   87
c ---[  49]---> BDD-cost:   87
c ---[  48]---> BDD-cost:   87
c ---[  47]---> BDD-cost:   87
c ---[  46]---> BDD-cost:   87
c ---[  45]---> BDD-cost:   87
c ---[  44]---> BDD-cost:   41
c ---[  43]---> BDD-cost:   41
c ---[  42]---> BDD-cost:   41
c ---[  41]---> BDD-cost:   41
c ---[  40]---> BDD-cost:   41
c ---[  39]---> BDD-cost:   41
c ---[  38]---> BDD-cost:   41
c ---[  37]---> BDD-cost:   41
c ---[  36]---> BDD-cost:   41
c ---[  35]---> BDD-cost:   41
c ---[  34]---> BDD-cost:   41
c ---[  33]---> BDD-cost:   41
c ---[  32]---> BDD-cost:   41
c ---[  31]---> BDD-cost:   41
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.84 0.94 0.90 2/54 2588
Raw data (stat): 2588 (runsolver) R 2587 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421774819 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0008 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 4024 0 0 0 987 10 0 0 25 0 1 0 421774819 18436096 3960 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4501 3960 603 41 0 4460 0
vsize: 18004
[startup+20.0009 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 5619 0 0 0 1984 14 0 0 25 0 1 0 421774819 25096192 5555 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6127 5555 603 41 0 6086 0
vsize: 24508
[startup+30.0017 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 7448 0 0 0 2981 17 0 0 25 0 1 0 421774819 32567296 7384 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7951 7384 603 41 0 7910 0
vsize: 31804
[startup+40.0012 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 8932 0 0 0 3976 22 0 0 25 0 1 0 421774819 38641664 8868 4294967295 134512640 134672761 3221224528 3221223712 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9434 8868 603 41 0 9393 0
vsize: 37736
[startup+50.0014 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 10821 0 0 0 4972 26 0 0 25 0 1 0 421774819 46350336 10756 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11316 10756 603 41 0 11275 0
vsize: 45264
[startup+60.0022 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 10821 0 0 0 5973 26 0 0 25 0 1 0 421774819 46350336 10756 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11316 10756 603 41 0 11275 0
vsize: 45264
[startup+70.0017 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 10821 0 0 0 6973 26 0 0 25 0 1 0 421774819 46350336 10756 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11316 10756 603 41 0 11275 0
vsize: 45264
[startup+80.0029 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 11661 0 0 0 7971 28 0 0 25 0 1 0 421774819 49811456 11596 4294967295 134512640 134672761 3221224528 3221223712 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12161 11596 603 41 0 12120 0
vsize: 48644
[startup+90.0027 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 12581 0 0 0 8967 32 0 0 25 0 1 0 421774819 53641216 12516 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13096 12516 603 41 0 13055 0
vsize: 52384
[startup+100.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 12841 0 0 0 9967 32 0 0 25 0 1 0 421774819 54624256 12775 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13336 12775 603 41 0 13295 0
vsize: 53344
[startup+110.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 12841 0 0 0 10967 32 0 0 25 0 1 0 421774819 54624256 12775 4294967295 134512640 134672761 3221224528 3221223568 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13336 12775 603 41 0 13295 0
vsize: 53344
[startup+120.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 12841 0 0 0 11967 32 0 0 25 0 1 0 421774819 54624256 12775 4294967295 134512640 134672761 3221224528 3221223712 134615689 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13336 12775 603 41 0 13295 0
vsize: 53344
[startup+130.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 12841 0 0 0 12968 32 0 0 25 0 1 0 421774819 54624256 12775 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13336 12775 603 41 0 13295 0
vsize: 53344
[startup+140.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 12841 0 0 0 13968 32 0 0 25 0 1 0 421774819 54624256 12775 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13336 12775 603 41 0 13295 0
vsize: 53344
[startup+150.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 12842 0 0 0 14968 32 0 0 25 0 1 0 421774819 54624256 12776 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13336 12776 603 41 0 13295 0
vsize: 53344
[startup+160.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 12844 0 0 0 15968 32 0 0 25 0 1 0 421774819 54579200 12772 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13325 12772 603 41 0 13284 0
vsize: 53300
[startup+170.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 12844 0 0 0 16968 33 0 0 25 0 1 0 421774819 54579200 12772 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13325 12772 603 41 0 13284 0
vsize: 53300
[startup+180.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 12844 0 0 0 17968 33 0 0 25 0 1 0 421774819 54579200 12772 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13325 12772 603 41 0 13284 0
vsize: 53300
[startup+190.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 12844 0 0 0 18969 33 0 0 25 0 1 0 421774819 54579200 12772 4294967295 134512640 134672761 3221224528 3221223712 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13325 12772 603 41 0 13284 0
vsize: 53300
[startup+200.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 12844 0 0 0 19969 33 0 0 25 0 1 0 421774819 54579200 12772 4294967295 134512640 134672761 3221224528 3221223712 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13325 12772 603 41 0 13284 0
vsize: 53300
[startup+210.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 12844 0 0 0 20969 33 0 0 25 0 1 0 421774819 54579200 12772 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13325 12772 603 41 0 13284 0
vsize: 53300
[startup+220.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 12844 0 0 0 21969 33 0 0 25 0 1 0 421774819 54579200 12772 4294967295 134512640 134672761 3221224528 3221223520 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13325 12772 603 41 0 13284 0
vsize: 53300
[startup+230.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 12844 0 0 0 22969 33 0 0 25 0 1 0 421774819 54579200 12772 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13325 12772 603 41 0 13284 0
vsize: 53300
[startup+240.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 12844 0 0 0 23970 33 0 0 25 0 1 0 421774819 54579200 12772 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13325 12772 603 41 0 13284 0
vsize: 53300
[startup+250.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 13332 0 0 0 24969 33 0 0 25 0 1 0 421774819 56696832 13260 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13842 13260 603 41 0 13801 0
vsize: 55368
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 13890 0 0 0 25967 35 0 0 25 0 1 0 421774819 58966016 13818 4294967295 134512640 134672761 3221224528 3221223712 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14396 13818 603 41 0 14355 0
vsize: 57584
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 14283 0 0 0 26967 36 0 0 25 0 1 0 421774819 60555264 14210 4294967295 134512640 134672761 3221224528 3221223712 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14784 14210 603 41 0 14743 0
vsize: 59136
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 14284 0 0 0 27967 36 0 0 25 0 1 0 421774819 60555264 14211 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14784 14211 603 41 0 14743 0
vsize: 59136
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 14287 0 0 0 28967 36 0 0 25 0 1 0 421774819 60555264 14214 4294967295 134512640 134672761 3221224528 3221223712 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14784 14214 603 41 0 14743 0
vsize: 59136
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 14292 0 0 0 29967 36 0 0 25 0 1 0 421774819 60555264 14219 4294967295 134512640 134672761 3221224528 3221223568 134612848 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14784 14219 603 41 0 14743 0
vsize: 59136
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 14292 0 0 0 30967 36 0 0 25 0 1 0 421774819 60555264 14219 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14784 14219 603 41 0 14743 0
vsize: 59136
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 14293 0 0 0 31968 36 0 0 25 0 1 0 421774819 60555264 14220 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14784 14220 603 41 0 14743 0
vsize: 59136
[startup+330.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 14293 0 0 0 32968 36 0 0 25 0 1 0 421774819 60555264 14220 4294967295 134512640 134672761 3221224528 3221223712 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14784 14220 603 41 0 14743 0
vsize: 59136
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 14294 0 0 0 33968 36 0 0 25 0 1 0 421774819 60555264 14221 4294967295 134512640 134672761 3221224528 3221223712 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14784 14221 603 41 0 14743 0
vsize: 59136
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 14294 0 0 0 34968 36 0 0 25 0 1 0 421774819 60555264 14221 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14784 14221 603 41 0 14743 0
vsize: 59136
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 14295 0 0 0 35968 36 0 0 25 0 1 0 421774819 60555264 14222 4294967295 134512640 134672761 3221224528 3221223712 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14784 14222 603 41 0 14743 0
vsize: 59136
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 14299 0 0 0 36969 36 0 0 25 0 1 0 421774819 60555264 14226 4294967295 134512640 134672761 3221224528 3221223712 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14784 14226 603 41 0 14743 0
vsize: 59136
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 14299 0 0 0 37969 36 0 0 25 0 1 0 421774819 60555264 14226 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14784 14226 603 41 0 14743 0
vsize: 59136
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 14300 0 0 0 38969 36 0 0 25 0 1 0 421774819 60555264 14227 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14784 14227 603 41 0 14743 0
vsize: 59136
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 14303 0 0 0 39969 36 0 0 25 0 1 0 421774819 60555264 14230 4294967295 134512640 134672761 3221224528 3221223712 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14784 14230 603 41 0 14743 0
vsize: 59136
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 14588 0 0 0 40968 37 0 0 25 0 1 0 421774819 61771776 14515 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15081 14515 603 41 0 15040 0
vsize: 60324
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 14917 0 0 0 41968 38 0 0 25 0 1 0 421774819 63098880 14844 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15405 14844 603 41 0 15364 0
vsize: 61620
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 15334 0 0 0 42967 38 0 0 25 0 1 0 421774819 64815104 15261 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15824 15261 603 41 0 15783 0
vsize: 63296
[startup+440.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 15901 0 0 0 43966 40 0 0 25 0 1 0 421774819 67198976 15828 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16406 15828 603 41 0 16365 0
vsize: 65624
[startup+450.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 15933 0 0 0 44966 40 0 0 25 0 1 0 421774819 67256320 15859 4294967295 134512640 134672761 3221224528 3221223728 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16420 15859 603 41 0 16379 0
vsize: 65680
[startup+460.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 15933 0 0 0 45967 40 0 0 25 0 1 0 421774819 67256320 15859 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16420 15859 603 41 0 16379 0
vsize: 65680
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 15933 0 0 0 46967 40 0 0 25 0 1 0 421774819 67256320 15859 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16420 15859 603 41 0 16379 0
vsize: 65680
[startup+480.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 15933 0 0 0 47967 40 0 0 25 0 1 0 421774819 67256320 15859 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16420 15859 603 41 0 16379 0
vsize: 65680
[startup+490.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 16940 0 0 0 48964 43 0 0 25 0 1 0 421774819 71471104 16866 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17449 16866 603 41 0 17408 0
vsize: 69796
[startup+500.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 17936 0 0 0 49962 45 0 0 25 0 1 0 421774819 75567104 17862 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18449 17862 603 41 0 18408 0
vsize: 73796
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 19087 0 0 0 50960 47 0 0 25 0 1 0 421774819 80330752 19013 4294967295 134512640 134672761 3221224528 3221223712 134615635 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19612 19013 603 41 0 19571 0
vsize: 78448
[startup+520.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 19304 0 0 0 51960 48 0 0 25 0 1 0 421774819 81096704 19230 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19799 19230 603 41 0 19758 0
vsize: 79196
[startup+530.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 19304 0 0 0 52960 48 0 0 25 0 1 0 421774819 81096704 19230 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19799 19230 603 41 0 19758 0
vsize: 79196
[startup+540.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 19304 0 0 0 53960 48 0 0 25 0 1 0 421774819 81096704 19230 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19799 19230 603 41 0 19758 0
vsize: 79196
[startup+550.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 19304 0 0 0 54960 48 0 0 25 0 1 0 421774819 81096704 19230 4294967295 134512640 134672761 3221224528 3221223568 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19799 19230 603 41 0 19758 0
vsize: 79196
[startup+560.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 19304 0 0 0 55960 48 0 0 25 0 1 0 421774819 81096704 19230 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19799 19230 603 41 0 19758 0
vsize: 79196
[startup+570.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 19304 0 0 0 56961 48 0 0 25 0 1 0 421774819 81096704 19230 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19799 19230 603 41 0 19758 0
vsize: 79196
[startup+580.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 19304 0 0 0 57961 48 0 0 25 0 1 0 421774819 81096704 19230 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19799 19230 603 41 0 19758 0
vsize: 79196
[startup+590.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 19304 0 0 0 58961 48 0 0 25 0 1 0 421774819 81096704 19230 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19799 19230 603 41 0 19758 0
vsize: 79196
[startup+600.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 19304 0 0 0 59961 48 0 0 25 0 1 0 421774819 81096704 19230 4294967295 134512640 134672761 3221224528 3221223712 134615581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19799 19230 603 41 0 19758 0
vsize: 79196
[startup+610.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 19305 0 0 0 60961 48 0 0 25 0 1 0 421774819 81096704 19231 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19799 19231 603 41 0 19758 0
vsize: 79196
[startup+620.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 19599 0 0 0 61960 49 0 0 25 0 1 0 421774819 82415616 19525 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20121 19525 603 41 0 20080 0
vsize: 80484
[startup+630.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 20361 0 0 0 62959 50 0 0 25 0 1 0 421774819 85573632 20287 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20892 20287 603 41 0 20851 0
vsize: 83568
[startup+640.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 21335 0 0 0 63957 52 0 0 25 0 1 0 421774819 89526272 21261 4294967295 134512640 134672761 3221224528 3221223712 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21857 21261 603 41 0 21816 0
vsize: 87428
[startup+650.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22223 0 0 0 64954 55 0 0 25 0 1 0 421774819 93208576 22149 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22756 22149 603 41 0 22715 0
vsize: 91024
[startup+660.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22712 0 0 0 65953 56 0 0 25 0 1 0 421774819 95125504 22637 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23224 22637 603 41 0 23183 0
vsize: 92896
[startup+670.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22712 0 0 0 66954 56 0 0 25 0 1 0 421774819 95125504 22637 4294967295 134512640 134672761 3221224528 3221223520 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23224 22637 603 41 0 23183 0
vsize: 92896
[startup+680.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22712 0 0 0 67954 56 0 0 25 0 1 0 421774819 95125504 22637 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23224 22637 603 41 0 23183 0
vsize: 92896
[startup+690.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22712 0 0 0 68954 56 0 0 25 0 1 0 421774819 95125504 22637 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23224 22637 603 41 0 23183 0
vsize: 92896
[startup+700.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22712 0 0 0 69954 56 0 0 25 0 1 0 421774819 95125504 22637 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23224 22637 603 41 0 23183 0
vsize: 92896
[startup+710.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22712 0 0 0 70954 56 0 0 25 0 1 0 421774819 95125504 22637 4294967295 134512640 134672761 3221224528 3221223712 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23224 22637 603 41 0 23183 0
vsize: 92896
[startup+720.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22712 0 0 0 71954 56 0 0 25 0 1 0 421774819 95125504 22637 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23224 22637 603 41 0 23183 0
vsize: 92896
[startup+730.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22712 0 0 0 72955 56 0 0 25 0 1 0 421774819 95125504 22637 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23224 22637 603 41 0 23183 0
vsize: 92896
[startup+740.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22712 0 0 0 73955 56 0 0 25 0 1 0 421774819 95117312 22635 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22635 603 41 0 23181 0
vsize: 92888
[startup+750.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22712 0 0 0 74955 56 0 0 25 0 1 0 421774819 95117312 22635 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22635 603 41 0 23181 0
vsize: 92888
[startup+760.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22712 0 0 0 75955 56 0 0 25 0 1 0 421774819 95117312 22635 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22635 603 41 0 23181 0
vsize: 92888
[startup+770.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22712 0 0 0 76955 56 0 0 25 0 1 0 421774819 95117312 22635 4294967295 134512640 134672761 3221224528 3221223712 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22635 603 41 0 23181 0
vsize: 92888
[startup+780.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22712 0 0 0 77956 56 0 0 25 0 1 0 421774819 95117312 22635 4294967295 134512640 134672761 3221224528 3221223712 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22635 603 41 0 23181 0
vsize: 92888
[startup+790.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22712 0 0 0 78956 56 0 0 25 0 1 0 421774819 95117312 22635 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22635 603 41 0 23181 0
vsize: 92888
[startup+800.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22712 0 0 0 79956 56 0 0 25 0 1 0 421774819 95117312 22635 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22635 603 41 0 23181 0
vsize: 92888
[startup+810.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22712 0 0 0 80956 56 0 0 25 0 1 0 421774819 95117312 22635 4294967295 134512640 134672761 3221224528 3221223712 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22635 603 41 0 23181 0
vsize: 92888
[startup+820.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22712 0 0 0 81956 56 0 0 25 0 1 0 421774819 95117312 22635 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22635 603 41 0 23181 0
vsize: 92888
[startup+830.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22712 0 0 0 82957 56 0 0 25 0 1 0 421774819 95117312 22635 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22635 603 41 0 23181 0
vsize: 92888
[startup+840.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22714 0 0 0 83957 56 0 0 25 0 1 0 421774819 95117312 22637 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22637 603 41 0 23181 0
vsize: 92888
[startup+850.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22714 0 0 0 84957 56 0 0 25 0 1 0 421774819 95117312 22637 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22637 603 41 0 23181 0
vsize: 92888
[startup+860.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22714 0 0 0 85957 56 0 0 25 0 1 0 421774819 95117312 22637 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22637 603 41 0 23181 0
vsize: 92888
[startup+870.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22714 0 0 0 86957 56 0 0 25 0 1 0 421774819 95117312 22637 4294967295 134512640 134672761 3221224528 3221223712 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22637 603 41 0 23181 0
vsize: 92888
[startup+880.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22714 0 0 0 87958 56 0 0 25 0 1 0 421774819 95117312 22637 4294967295 134512640 134672761 3221224528 3221223712 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22637 603 41 0 23181 0
vsize: 92888
[startup+890.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22714 0 0 0 88958 56 0 0 25 0 1 0 421774819 95117312 22637 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22637 603 41 0 23181 0
vsize: 92888
[startup+900.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22714 0 0 0 89958 56 0 0 25 0 1 0 421774819 95117312 22637 4294967295 134512640 134672761 3221224528 3221223712 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22637 603 41 0 23181 0
vsize: 92888
[startup+910.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22714 0 0 0 90958 56 0 0 25 0 1 0 421774819 95117312 22637 4294967295 134512640 134672761 3221224528 3221223712 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22637 603 41 0 23181 0
vsize: 92888
[startup+920.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22714 0 0 0 91958 56 0 0 25 0 1 0 421774819 95117312 22637 4294967295 134512640 134672761 3221224528 3221223712 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22637 603 41 0 23181 0
vsize: 92888
[startup+930.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22714 0 0 0 92958 56 0 0 25 0 1 0 421774819 95117312 22637 4294967295 134512640 134672761 3221224528 3221223584 134644266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22637 603 41 0 23181 0
vsize: 92888
[startup+940.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22714 0 0 0 93959 56 0 0 25 0 1 0 421774819 95117312 22637 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22637 603 41 0 23181 0
vsize: 92888
[startup+950.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22714 0 0 0 94959 56 0 0 25 0 1 0 421774819 95117312 22637 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22637 603 41 0 23181 0
vsize: 92888
[startup+960.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22717 0 0 0 95959 56 0 0 25 0 1 0 421774819 95117312 22640 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22640 603 41 0 23181 0
vsize: 92888
[startup+970.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22717 0 0 0 96959 56 0 0 25 0 1 0 421774819 95117312 22640 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22640 603 41 0 23181 0
vsize: 92888
[startup+980.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22717 0 0 0 97960 56 0 0 25 0 1 0 421774819 95117312 22640 4294967295 134512640 134672761 3221224528 3221223712 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22640 603 41 0 23181 0
vsize: 92888
[startup+990.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22717 0 0 0 98960 56 0 0 25 0 1 0 421774819 95117312 22640 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22640 603 41 0 23181 0
vsize: 92888
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22717 0 0 0 99960 56 0 0 25 0 1 0 421774819 95117312 22640 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22640 603 41 0 23181 0
vsize: 92888
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22717 0 0 0 100960 56 0 0 25 0 1 0 421774819 95117312 22640 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22640 603 41 0 23181 0
vsize: 92888
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2588
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22717 0 0 0 101960 56 0 0 25 0 1 0 421774819 95117312 22640 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22640 603 41 0 23181 0
vsize: 92888
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 3/57 2623
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22717 0 0 0 102961 56 0 0 25 0 1 0 421774819 95117312 22640 4294967295 134512640 134672761 3221224528 3221223712 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22640 603 41 0 23181 0
vsize: 92888
[startup+1040.03 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 2641
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22717 0 0 0 103960 56 0 0 25 0 1 0 421774819 95117312 22640 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22640 603 41 0 23181 0
vsize: 92888
[startup+1050.03 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 2641
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22717 0 0 0 104960 56 0 0 25 0 1 0 421774819 95117312 22640 4294967295 134512640 134672761 3221224528 3221223712 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22640 603 41 0 23181 0
vsize: 92888
[startup+1060.03 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 2641
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22717 0 0 0 105961 56 0 0 25 0 1 0 421774819 95117312 22640 4294967295 134512640 134672761 3221224528 3221223712 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22640 603 41 0 23181 0
vsize: 92888
[startup+1070.03 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 2641
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22717 0 0 0 106961 56 0 0 25 0 1 0 421774819 95117312 22640 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22640 603 41 0 23181 0
vsize: 92888
[startup+1080.03 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 2641
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22717 0 0 0 107961 56 0 0 25 0 1 0 421774819 95117312 22640 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22640 603 41 0 23181 0
vsize: 92888
[startup+1090.03 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 2641
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22717 0 0 0 108961 56 0 0 25 0 1 0 421774819 95117312 22640 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22640 603 41 0 23181 0
vsize: 92888
[startup+1100.03 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 2643
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22717 0 0 0 109961 56 0 0 25 0 1 0 421774819 95117312 22640 4294967295 134512640 134672761 3221224528 3221223712 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22640 603 41 0 23181 0
vsize: 92888
[startup+1110.03 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 2643
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22717 0 0 0 110962 56 0 0 25 0 1 0 421774819 95117312 22640 4294967295 134512640 134672761 3221224528 3221223712 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22640 603 41 0 23181 0
vsize: 92888
[startup+1120.03 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 2643
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22717 0 0 0 111962 56 0 0 25 0 1 0 421774819 95117312 22640 4294967295 134512640 134672761 3221224528 3221223712 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22640 603 41 0 23181 0
vsize: 92888
[startup+1130.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 2643
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22717 0 0 0 112962 56 0 0 25 0 1 0 421774819 95117312 22640 4294967295 134512640 134672761 3221224528 3221223712 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22640 603 41 0 23181 0
vsize: 92888
[startup+1140.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 2643
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22717 0 0 0 113962 56 0 0 25 0 1 0 421774819 95117312 22640 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22640 603 41 0 23181 0
vsize: 92888
[startup+1150.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 2643
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22717 0 0 0 114962 56 0 0 25 0 1 0 421774819 95117312 22640 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22640 603 41 0 23181 0
vsize: 92888
[startup+1160.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 2643
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22717 0 0 0 115963 56 0 0 25 0 1 0 421774819 95117312 22640 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22640 603 41 0 23181 0
vsize: 92888
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2643
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22717 0 0 0 116963 56 0 0 25 0 1 0 421774819 95117312 22640 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22640 603 41 0 23181 0
vsize: 92888
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2643
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22717 0 0 0 117963 56 0 0 25 0 1 0 421774819 95117312 22640 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22640 603 41 0 23181 0
vsize: 92888
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2643
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22717 0 0 0 118963 56 0 0 25 0 1 0 421774819 95117312 22640 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22640 603 41 0 23181 0
vsize: 92888
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2643
Raw data (stat): 2588 (minisat+) R 2587 29151 29150 0 -1 0 22717 0 0 0 119963 56 0 0 25 0 1 0 421774819 95117312 22640 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23222 22640 603 41 0 23181 0
vsize: 92888
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 2643
Raw data (stat): 2588 (minisat+) Z 2587 29151 29150 0 -1 12 22717 0 0 0 119963 61 0 0 25 0 1 0 421774819 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.08
CPU time (s): 1200.25
CPU user time (s): 1199.64
CPU system time (s): 0.611906
CPU usage (%): 100.014
Max. virtual memory (Kb): 92896
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####