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-chnl50_55_pb.cnf.cr.opb
MD5SUM	88aaed929c30a489c8806c3852596de3
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
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	56
Number of bits of the biggest sum of numbers	6
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.173973
Number of variables	5500
Total number of constraints	210
Number of constraints which are clauses	110
Number of constraints which are cardinality constraints (but not clauses)	100
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	50
Maximum length of a constraint	55
Trace number 6155

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc32 THE 2005-04-14 03:32:05 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4533 boxname=wulflinc32 idbench=21 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  88aaed929c30a489c8806c3852596de3  /oldhome/oroussel/tmp/wulflinc32/normalized-chnl50_55_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc32/normalized-chnl50_55_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc32/normalized-chnl50_55_pb.cnf.cr.opb
IDLAUNCH: 4533
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.085
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.085
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:      1034724 kB
MemFree:        702508 kB
Buffers:         35264 kB
Cached:         185544 kB
SwapCached:       1212 kB
Active:         146936 kB
Inactive:       154240 kB
HighTotal:      131072 kB
HighFree:          256 kB
LowTotal:       903652 kB
LowFree:        702252 kB
SwapTotal:     2097892 kB
SwapFree:      2096680 kB
Dirty:            2340 kB
Writeback:           0 kB
Mapped:          81768 kB
Slab:            25372 kB
Committed_AS:   174000 kB
PageTables:        432 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 03:52:08 (client local time) WITH STATUS 0 IN 1200.28 SECONDS
stats: 4533 7 1200.28 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 210 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..............................................................................................................
c ---[  99]---> BDD-cost:  107
c ---[  98]---> BDD-cost:  107
c ---[  97]---> BDD-cost:  107
c ---[  96]---> BDD-cost:  107
c ---[  95]---> BDD-cost:  107
c ---[  94]---> BDD-cost:  107
c ---[  93]---> BDD-cost:  107
c ---[  92]---> BDD-cost:  107
c ---[  91]---> BDD-cost:  107
c ---[  90]---> BDD-cost:  107
c ---[  89]---> BDD-cost:  107
c ---[  88]---> BDD-cost:  107
c ---[  87]---> BDD-cost:  107
c ---[  86]---> BDD-cost:  107
c ---[  85]---> BDD-cost:  107
c ---[  84]---> BDD-cost:  107
c ---[  83]---> BDD-cost:  107
c ---[  82]---> BDD-cost:  107
c ---[  81]---> BDD-cost:  107
c ---[  80]---> BDD-cost:  107
c ---[  79]---> BDD-cost:  107
c ---[  78]---> BDD-cost:  107
c ---[  77]---> BDD-cost:  107
c ---[  76]---> BDD-cost:  107
c ---[  75]---> BDD-cost:  107
c ---[  74]---> BDD-cost:  107
c ---[  73]---> BDD-cost:  107
c ---[  72]---> BDD-cost:  107
c ---[  71]---> BDD-cost:  107
c ---[  70]---> BDD-cost:  107
c ---[  69]---> BDD-cost:  107
c ---[  68]---> BDD-cost:  107
c ---[  67]---> BDD-cost:  107
c ---[  66]---> BDD-cost:  107
c ---[  65]---> BDD-cost:  107
c ---[  64]---> BDD-cost:  107
c ---[  63]---> BDD-cost:  107
c ---[  62]---> BDD-cost:  107
c ---[  61]---> BDD-cost:  107
c ---[  60]---> BDD-cost:  107
c ---[  59]---> BDD-cost:  107
c ---[  58]---> BDD-cost:  107
c ---[  57]---> BDD-cost:  107
c ---[  56]---> BDD-cost:  107
c ---[  55]---> BDD-cost:  107
c ---[  54]---> BDD-cost:  107
c ---[  53]---> BDD-cost:  107
c ---[  52]---> BDD-cost:  107
c ---[  51]---> BDD-cost:  107
c ---[  50]---> BDD-cost:  107
c ---[  49]---> BDD-cost:  107
c ---[  48]---> BDD-cost:  107
c ---[  47]---> BDD-cost:  107
c ---[  46]---> BDD-cost:  107
c ---[  45]---> BDD-cost:  107
c ---[  44]---> BDD-cost:  107
c ---[  43]---> BDD-cost:  107
c ---[  42]---> BDD-cost:  107
c ---[  41]---> BDD-cost:  107
c ---[  40]---> BDD-cost:  107
c ---[  39]---> BDD-cost:  107
c ---[  38]---> BDD-cost:  107
c ---[  37]---> BDD-cost:  107
c ---[  36]---> BDD-cost:  107
c ---[  35]---> BDD-cost:  107
c ---[  34]---> BDD-cost:  107
c ---[  33]---> BDD-cost:  107
c ---[  32]---> BDD-cost:  107
c ---[  31]---> BDD-cost:  107
c ---[  30]---> BDD-cost:  107
c ---[  29]---> BDD-cost:  107
c ---[  28]---> BDD-cost:  107
c ---[  27]---> BDD-cost:  107
c ---[  26]---> BDD-cost:  107
c ---[  25]---> BDD-cost:  107
c ---[  24]---> BDD-cost:  107
c ---[  23]---> BDD-cost:  107
c ---[  22]---> BDD-cost:  107
c ---[  21]---> BDD-cost:  107
c ---[  20]---> BDD-cost:  107
c ---[  19]---> BDD-cost:  107
c ---[  18]---> BDD-cost:  107
c ---[  17]---> BDD-cost:  107
c ---[  16]---> BDD-cost:  107
c ---[  15]---> BDD-cost:  107
c ---[  14]---> BDD-cost:  107
c ---[  13]---> BDD-cost:  107
c ---[  12]---> BDD-cost:  107
c ---[  11]---> BDD-cost:  107
c ---[  10]---> BDD-cost:  107
c ---[   9]---> BDD-cost:  107
c ---[   8]---> BDD-cost:  107
c ---[   7]---> BDD-cost:  107
c ---[   6]---> BDD-cost:  107
c ---[   5]---> BDD-cost:  107
c ---[   4]---> BDD-cost:  107
c ---[   3]---> BDD-cost:  107
c ---[   2]---> BDD-cost:  107
c ---[   1]---> BDD-cost:  107
c ---[   0]---> BDD-cost:  107
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   47810   137800 |   15936       0        0     nan |  0.000 % |
c |       100 |   47600   137170 |   17529      14       40     2.9 |  0.877 % |
c |       252 |   47305   136285 |   19282      30       83     2.8 |  1.247 % |
c |       477 |   46805   134785 |   21210      61      177     2.9 |  1.864 % |
c |       814 |   45891   132045 |   23331      84      276     3.3 |  2.988 % |
c |      1322 |   45361   130455 |   25665     400    79019   197.5 |  3.642 % |
c |      2083 |   45246   130110 |   28231    1124   257131   228.8 |  3.784 % |
c |      3226 |   44741   128595 |   31054    2093   507318   242.4 |  4.407 % |
c |      4936 |   43751   125625 |   34160    3449   900111   261.0 |  5.630 % |
c |      7498 |   43701   125475 |   37576    5995  1904351   317.7 |  5.691 % |
c |     11343 |   39807   113795 |   41333    8584  2788459   324.8 | 10.500 % |
c |     17109 |   36623   104245 |   45467   13278  4698280   353.8 | 14.438 % |
c |     25759 |   34083    96625 |   50013   21058  7567682   359.4 | 17.568 % |
c |     38733 |   30023    84445 |   55015   32754 12778042   390.1 | 22.580 % |
c |     58194 |   27564    77070 |   60516   51442 20285378   394.3 | 25.617 % |
#### 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.91 2/53 14687
Raw data (stat): 14687 (runsolver) R 14686 7987 7986 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481369752 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0014 s]
Raw data (loadavg): 0.93 0.95 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 1706 0 0 0 994 4 0 0 25 0 1 0 481369752 8499200 1638 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2075 1638 603 41 0 2034 0
vsize: 8300
[startup+20.0019 s]
Raw data (loadavg): 0.94 0.96 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 2333 0 0 0 1992 5 0 0 25 0 1 0 481369752 11059200 2265 4294967295 134512640 134672761 3221224544 3221223668 134566080 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2700 2265 603 41 0 2659 0
vsize: 10800
[startup+30.0039 s]
Raw data (loadavg): 0.95 0.96 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 3255 0 0 0 2990 7 0 0 25 0 1 0 481369752 14843904 3187 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3624 3187 603 41 0 3583 0
vsize: 14496
[startup+40.0044 s]
Raw data (loadavg): 0.95 0.96 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 3775 0 0 0 3988 9 0 0 25 0 1 0 481369752 17002496 3707 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4151 3707 603 41 0 4110 0
vsize: 16604
[startup+50.0062 s]
Raw data (loadavg): 0.96 0.96 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 3994 0 0 0 4988 9 0 0 25 0 1 0 481369752 17809408 3926 4294967295 134512640 134672761 3221224544 3221223716 134556596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4348 3926 603 41 0 4307 0
vsize: 17392
[startup+60.007 s]
Raw data (loadavg): 0.97 0.96 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 4003 0 0 0 5988 10 0 0 25 0 1 0 481369752 17944576 3935 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4381 3935 603 41 0 4340 0
vsize: 17524
[startup+70.0078 s]
Raw data (loadavg): 0.97 0.96 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 4204 0 0 0 6988 10 0 0 25 0 1 0 481369752 18751488 4136 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4578 4136 603 41 0 4537 0
vsize: 18312
[startup+80.0095 s]
Raw data (loadavg): 0.98 0.96 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 4470 0 0 0 7988 10 0 0 25 0 1 0 481369752 19828736 4402 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4841 4402 603 41 0 4800 0
vsize: 19364
[startup+90.0103 s]
Raw data (loadavg): 0.98 0.96 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 4483 0 0 0 8988 10 0 0 25 0 1 0 481369752 19828736 4415 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4841 4415 603 41 0 4800 0
vsize: 19364
[startup+100.011 s]
Raw data (loadavg): 0.98 0.96 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 4671 0 0 0 9988 11 0 0 25 0 1 0 481369752 20635648 4603 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5038 4603 603 41 0 4997 0
vsize: 20152
[startup+110.012 s]
Raw data (loadavg): 0.98 0.96 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 4727 0 0 0 10988 11 0 0 25 0 1 0 481369752 20905984 4659 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5104 4659 603 41 0 5063 0
vsize: 20416
[startup+120.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 5090 0 0 0 11987 12 0 0 25 0 1 0 481369752 22392832 5022 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5467 5022 603 41 0 5426 0
vsize: 21868
[startup+130.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 5090 0 0 0 12986 12 0 0 25 0 1 0 481369752 22392832 5022 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5467 5022 603 41 0 5426 0
vsize: 21868
[startup+140.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 5141 0 0 0 13987 12 0 0 25 0 1 0 481369752 22528000 5073 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5500 5073 603 41 0 5459 0
vsize: 22000
[startup+150.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 5340 0 0 0 14987 12 0 0 25 0 1 0 481369752 23339008 5272 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5698 5272 603 41 0 5657 0
vsize: 22792
[startup+160.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 6414 0 0 0 15983 16 0 0 25 0 1 0 481369752 27799552 6346 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6787 6346 603 41 0 6746 0
vsize: 27148
[startup+170.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 6606 0 0 0 16983 16 0 0 25 0 1 0 481369752 28610560 6538 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6985 6538 603 41 0 6944 0
vsize: 27940
[startup+180.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 6685 0 0 0 17983 16 0 0 25 0 1 0 481369752 28880896 6617 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7051 6617 603 41 0 7010 0
vsize: 28204
[startup+190.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 6752 0 0 0 18983 16 0 0 25 0 1 0 481369752 29151232 6684 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7117 6684 603 41 0 7076 0
vsize: 28468
[startup+200.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 6808 0 0 0 19982 17 0 0 25 0 1 0 481369752 29421568 6740 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7183 6740 603 41 0 7142 0
vsize: 28732
[startup+210.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 6892 0 0 0 20982 17 0 0 25 0 1 0 481369752 29691904 6824 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7249 6825 603 41 0 7208 0
vsize: 28996
[startup+220.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 7003 0 0 0 21981 17 0 0 25 0 1 0 481369752 30232576 6935 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7381 6935 603 41 0 7340 0
vsize: 29524
[startup+230.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 7443 0 0 0 22980 19 0 0 25 0 1 0 481369752 31985664 7375 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7809 7375 603 41 0 7768 0
vsize: 31236
[startup+240.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 7570 0 0 0 23980 19 0 0 25 0 1 0 481369752 32522240 7502 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7940 7502 603 41 0 7899 0
vsize: 31760
[startup+250.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 7571 0 0 0 24980 19 0 0 25 0 1 0 481369752 32522240 7503 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7940 7503 603 41 0 7899 0
vsize: 31760
[startup+260.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 8146 0 0 0 25979 21 0 0 25 0 1 0 481369752 34816000 8078 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8500 8078 603 41 0 8459 0
vsize: 34000
[startup+270.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 8245 0 0 0 26978 21 0 0 25 0 1 0 481369752 35315712 8177 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8622 8177 603 41 0 8581 0
vsize: 34488
[startup+280.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 8432 0 0 0 27978 21 0 0 25 0 1 0 481369752 36126720 8364 4294967295 134512640 134672761 3221224544 3221223648 134559908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8820 8364 603 41 0 8779 0
vsize: 35280
[startup+290.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 8560 0 0 0 28978 22 0 0 25 0 1 0 481369752 36667392 8492 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8952 8492 603 41 0 8911 0
vsize: 35808
[startup+300.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 8671 0 0 0 29978 22 0 0 25 0 1 0 481369752 37072896 8603 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9051 8603 603 41 0 9010 0
vsize: 36204
[startup+310.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 8701 0 0 0 30978 22 0 0 25 0 1 0 481369752 37208064 8633 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9084 8633 603 41 0 9043 0
vsize: 36336
[startup+320.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 8778 0 0 0 31979 22 0 0 25 0 1 0 481369752 37478400 8710 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9150 8710 603 41 0 9109 0
vsize: 36600
[startup+330.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 9103 0 0 0 32978 23 0 0 25 0 1 0 481369752 38821888 9035 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9478 9035 603 41 0 9437 0
vsize: 37912
[startup+340.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 10059 0 0 0 33976 25 0 0 25 0 1 0 481369752 42741760 9991 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10435 9991 603 41 0 10394 0
vsize: 41740
[startup+350.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 10280 0 0 0 34976 25 0 0 25 0 1 0 481369752 43683840 10212 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10665 10212 603 41 0 10624 0
vsize: 42660
[startup+360.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 10328 0 0 0 35976 25 0 0 25 0 1 0 481369752 43819008 10260 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10698 10260 603 41 0 10657 0
vsize: 42792
[startup+370.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 10585 0 0 0 36975 27 0 0 25 0 1 0 481369752 44896256 10517 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10961 10517 603 41 0 10920 0
vsize: 43844
[startup+380.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 10996 0 0 0 37975 27 0 0 25 0 1 0 481369752 46505984 10928 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11354 10928 603 41 0 11313 0
vsize: 45416
[startup+390.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 10998 0 0 0 38975 27 0 0 25 0 1 0 481369752 46641152 10930 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11387 10930 603 41 0 11346 0
vsize: 45548
[startup+400.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 11021 0 0 0 39975 27 0 0 25 0 1 0 481369752 46641152 10953 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11387 10953 603 41 0 11346 0
vsize: 45548
[startup+410.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 11238 0 0 0 40975 28 0 0 25 0 1 0 481369752 47587328 11170 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11618 11170 603 41 0 11577 0
vsize: 46472
[startup+420.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 11343 0 0 0 41975 28 0 0 25 0 1 0 481369752 47992832 11275 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11717 11275 603 41 0 11676 0
vsize: 46868
[startup+430.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 11347 0 0 0 42975 28 0 0 25 0 1 0 481369752 47992832 11279 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11717 11279 603 41 0 11676 0
vsize: 46868
[startup+440.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 11519 0 0 0 43975 29 0 0 25 0 1 0 481369752 48668672 11451 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11882 11451 603 41 0 11841 0
vsize: 47528
[startup+450.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 11686 0 0 0 44975 29 0 0 25 0 1 0 481369752 49340416 11618 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12046 11618 603 41 0 12005 0
vsize: 48184
[startup+460.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 11688 0 0 0 45975 29 0 0 25 0 1 0 481369752 49340416 11620 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12046 11620 603 41 0 12005 0
vsize: 48184
[startup+470.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 11688 0 0 0 46975 29 0 0 25 0 1 0 481369752 49340416 11620 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12046 11620 603 41 0 12005 0
vsize: 48184
[startup+480.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 12169 0 0 0 47974 30 0 0 25 0 1 0 481369752 51363840 12101 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12540 12101 603 41 0 12499 0
vsize: 50160
[startup+490.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 12610 0 0 0 48973 31 0 0 25 0 1 0 481369752 53116928 12542 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12968 12542 603 41 0 12927 0
vsize: 51872
[startup+500.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 12611 0 0 0 49974 31 0 0 25 0 1 0 481369752 53116928 12543 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12968 12543 603 41 0 12927 0
vsize: 51872
[startup+510.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 12611 0 0 0 50974 31 0 0 25 0 1 0 481369752 53116928 12543 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12968 12543 603 41 0 12927 0
vsize: 51872
[startup+520.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 13035 0 0 0 51973 33 0 0 25 0 1 0 481369752 54870016 12967 4294967295 134512640 134672761 3221224544 3221223728 134558839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13396 12967 603 41 0 13355 0
vsize: 53584
[startup+530.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 14171 0 0 0 52971 35 0 0 25 0 1 0 481369752 59588608 14103 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14548 14103 603 41 0 14507 0
vsize: 58192
[startup+540.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 14386 0 0 0 53970 35 0 0 25 0 1 0 481369752 60395520 14318 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14745 14318 603 41 0 14704 0
vsize: 58980
[startup+550.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 14637 0 0 0 54970 36 0 0 25 0 1 0 481369752 61472768 14569 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15008 14569 603 41 0 14967 0
vsize: 60032
[startup+560.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 14767 0 0 0 55970 37 0 0 25 0 1 0 481369752 62013440 14699 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15140 14699 603 41 0 15099 0
vsize: 60560
[startup+570.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 14789 0 0 0 56970 37 0 0 25 0 1 0 481369752 62013440 14721 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15140 14721 603 41 0 15099 0
vsize: 60560
[startup+580.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 15129 0 0 0 57969 38 0 0 25 0 1 0 481369752 63496192 15061 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15502 15061 603 41 0 15461 0
vsize: 62008
[startup+590.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 15181 0 0 0 58969 38 0 0 25 0 1 0 481369752 63631360 15113 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15535 15113 603 41 0 15494 0
vsize: 62140
[startup+600.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 15191 0 0 0 59970 38 0 0 25 0 1 0 481369752 63766528 15123 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15568 15123 603 41 0 15527 0
vsize: 62272
[startup+610.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 15496 0 0 0 60969 39 0 0 25 0 1 0 481369752 64978944 15428 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15864 15428 603 41 0 15823 0
vsize: 63456
[startup+620.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 15524 0 0 0 61969 39 0 0 25 0 1 0 481369752 65114112 15456 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15897 15456 603 41 0 15856 0
vsize: 63588
[startup+630.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 15524 0 0 0 62969 39 0 0 25 0 1 0 481369752 65114112 15456 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15897 15456 603 41 0 15856 0
vsize: 63588
[startup+640.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 15600 0 0 0 63970 39 0 0 25 0 1 0 481369752 65384448 15532 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15963 15532 603 41 0 15922 0
vsize: 63852
[startup+650.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 15601 0 0 0 64970 39 0 0 25 0 1 0 481369752 65384448 15533 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15963 15533 603 41 0 15922 0
vsize: 63852
[startup+660.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 15835 0 0 0 65969 40 0 0 25 0 1 0 481369752 66457600 15767 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16225 15767 603 41 0 16184 0
vsize: 64900
[startup+670.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 15835 0 0 0 66969 40 0 0 25 0 1 0 481369752 66457600 15767 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16225 15767 603 41 0 16184 0
vsize: 64900
[startup+680.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 16340 0 0 0 67967 42 0 0 25 0 1 0 481369752 68612096 16272 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16751 16272 603 41 0 16710 0
vsize: 67004
[startup+690.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 16357 0 0 0 68968 42 0 0 25 0 1 0 481369752 68612096 16289 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16751 16289 603 41 0 16710 0
vsize: 67004
[startup+700.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 16358 0 0 0 69968 42 0 0 25 0 1 0 481369752 68612096 16290 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16751 16290 603 41 0 16710 0
vsize: 67004
[startup+710.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 16375 0 0 0 70968 42 0 0 25 0 1 0 481369752 68747264 16307 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16784 16307 603 41 0 16743 0
vsize: 67136
[startup+720.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 16558 0 0 0 71968 42 0 0 25 0 1 0 481369752 69423104 16490 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16949 16490 603 41 0 16908 0
vsize: 67796
[startup+730.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 17276 0 0 0 72967 43 0 0 25 0 1 0 481369752 72388608 17208 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17673 17208 603 41 0 17632 0
vsize: 70692
[startup+740.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 17949 0 0 0 73966 44 0 0 25 0 1 0 481369752 75091968 17881 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18333 17881 603 41 0 18292 0
vsize: 73332
[startup+750.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 18159 0 0 0 74966 45 0 0 25 0 1 0 481369752 76038144 18091 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18564 18091 603 41 0 18523 0
vsize: 74256
[startup+760.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 18189 0 0 0 75966 45 0 0 25 0 1 0 481369752 76038144 18121 4294967295 134512640 134672761 3221224544 3221223716 134556646 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18564 18121 603 41 0 18523 0
vsize: 74256
[startup+770.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 18878 0 0 0 76965 46 0 0 25 0 1 0 481369752 78876672 18810 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19257 18810 603 41 0 19216 0
vsize: 77028
[startup+780.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 19034 0 0 0 77965 47 0 0 25 0 1 0 481369752 79552512 18966 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19422 18966 603 41 0 19381 0
vsize: 77688
[startup+790.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 19292 0 0 0 78964 48 0 0 25 0 1 0 481369752 80633856 19224 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19686 19224 603 41 0 19645 0
vsize: 78744
[startup+800.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 19292 0 0 0 79964 48 0 0 25 0 1 0 481369752 80633856 19224 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19686 19224 603 41 0 19645 0
vsize: 78744
[startup+810.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 19414 0 0 0 80964 48 0 0 25 0 1 0 481369752 81174528 19346 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19818 19346 603 41 0 19777 0
vsize: 79272
[startup+820.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 20055 0 0 0 81963 50 0 0 25 0 1 0 481369752 83734528 19987 4294967295 134512640 134672761 3221224544 3221223648 134560267 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20443 19987 603 41 0 20402 0
vsize: 81772
[startup+830.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 20436 0 0 0 82962 50 0 0 25 0 1 0 481369752 85344256 20368 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20836 20368 603 41 0 20795 0
vsize: 83344
[startup+840.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 21421 0 0 0 83960 53 0 0 25 0 1 0 481369752 89260032 21353 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21792 21354 603 41 0 21751 0
vsize: 87168
[startup+850.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 22257 0 0 0 84959 54 0 0 25 0 1 0 481369752 92774400 22189 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22650 22189 603 41 0 22609 0
vsize: 90600
[startup+860.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 22425 0 0 0 85959 55 0 0 25 0 1 0 481369752 93442048 22357 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22813 22357 603 41 0 22772 0
vsize: 91252
[startup+870.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 22434 0 0 0 86959 55 0 0 25 0 1 0 481369752 93442048 22366 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22813 22366 603 41 0 22772 0
vsize: 91252
[startup+880.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 22998 0 0 0 87959 56 0 0 25 0 1 0 481369752 95727616 22930 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23371 22930 603 41 0 23330 0
vsize: 93484
[startup+890.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 23018 0 0 0 88959 56 0 0 25 0 1 0 481369752 95862784 22950 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23404 22950 603 41 0 23363 0
vsize: 93616
[startup+900.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 23168 0 0 0 89959 56 0 0 25 0 1 0 481369752 96403456 23100 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23536 23100 603 41 0 23495 0
vsize: 94144
[startup+910.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 23175 0 0 0 90959 56 0 0 25 0 1 0 481369752 96542720 23107 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23570 23107 603 41 0 23529 0
vsize: 94280
[startup+920.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 23351 0 0 0 91959 56 0 0 25 0 1 0 481369752 97218560 23283 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23735 23283 603 41 0 23694 0
vsize: 94940
[startup+930.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 23520 0 0 0 92959 56 0 0 25 0 1 0 481369752 97902592 23452 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23902 23452 603 41 0 23861 0
vsize: 95608
[startup+940.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 23913 0 0 0 93958 57 0 0 25 0 1 0 481369752 99520512 23845 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24297 23845 603 41 0 24256 0
vsize: 97188
[startup+950.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 23960 0 0 0 94958 58 0 0 25 0 1 0 481369752 99655680 23892 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24330 23892 603 41 0 24289 0
vsize: 97320
[startup+960.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 23966 0 0 0 95958 58 0 0 25 0 1 0 481369752 99790848 23898 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24363 23898 603 41 0 24322 0
vsize: 97452
[startup+970.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 23966 0 0 0 96958 58 0 0 25 0 1 0 481369752 99790848 23898 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24363 23898 603 41 0 24322 0
vsize: 97452
[startup+980.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 23966 0 0 0 97959 58 0 0 25 0 1 0 481369752 99790848 23898 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24363 23898 603 41 0 24322 0
vsize: 97452
[startup+990.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 24001 0 0 0 98958 58 0 0 25 0 1 0 481369752 99930112 23933 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24397 23933 603 41 0 24356 0
vsize: 97588
[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 24138 0 0 0 99957 59 0 0 25 0 1 0 481369752 100474880 24070 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24530 24070 603 41 0 24489 0
vsize: 98120
[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 24274 0 0 0 100957 59 0 0 25 0 1 0 481369752 101019648 24206 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24663 24206 603 41 0 24622 0
vsize: 98652
[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 24274 0 0 0 101957 59 0 0 25 0 1 0 481369752 101019648 24206 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24663 24206 603 41 0 24622 0
vsize: 98652
[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 25333 0 0 0 102954 63 0 0 25 0 1 0 481369752 105353216 25265 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25721 25265 603 41 0 25680 0
vsize: 102884
[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 25893 0 0 0 103953 64 0 0 25 0 1 0 481369752 107671552 25825 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26287 25825 603 41 0 26246 0
vsize: 105148
[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 26406 0 0 0 104952 66 0 0 25 0 1 0 481369752 109699072 26338 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26782 26338 603 41 0 26741 0
vsize: 107128
[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 26852 0 0 0 105951 67 0 0 25 0 1 0 481369752 111587328 26784 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27243 26784 603 41 0 27202 0
vsize: 108972
[startup+1070.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 27285 0 0 0 106950 68 0 0 25 0 1 0 481369752 113332224 27217 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27669 27217 603 41 0 27628 0
vsize: 110676
[startup+1080.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 27482 0 0 0 107950 68 0 0 25 0 1 0 481369752 114143232 27414 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27867 27414 603 41 0 27826 0
vsize: 111468
[startup+1090.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 28612 0 0 0 108947 71 0 0 25 0 1 0 481369752 118722560 28544 4294967295 134512640 134672761 3221224544 3221223648 134560355 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28985 28544 603 41 0 28944 0
vsize: 115940
[startup+1100.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 29121 0 0 0 109946 72 0 0 25 0 1 0 481369752 120881152 29053 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29512 29053 603 41 0 29471 0
vsize: 118048
[startup+1110.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 29869 0 0 0 110945 74 0 0 25 0 1 0 481369752 123981824 29801 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30269 29801 603 41 0 30228 0
vsize: 121076
[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 29876 0 0 0 111945 74 0 0 25 0 1 0 481369752 123981824 29808 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30269 29808 603 41 0 30228 0
vsize: 121076
[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 29876 0 0 0 112945 74 0 0 25 0 1 0 481369752 123981824 29808 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30269 29808 603 41 0 30228 0
vsize: 121076
[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 29877 0 0 0 113945 74 0 0 25 0 1 0 481369752 123981824 29809 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30269 29809 603 41 0 30228 0
vsize: 121076
[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 30165 0 0 0 114945 75 0 0 25 0 1 0 481369752 125202432 30097 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30567 30097 603 41 0 30526 0
vsize: 122268
[startup+1160.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 30553 0 0 0 115944 76 0 0 25 0 1 0 481369752 126685184 30485 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30929 30485 603 41 0 30888 0
vsize: 123716
[startup+1170.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 30647 0 0 0 116944 76 0 0 25 0 1 0 481369752 127090688 30579 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31028 30579 603 41 0 30987 0
vsize: 124112
[startup+1180.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 30861 0 0 0 117944 77 0 0 25 0 1 0 481369752 128040960 30793 4294967295 134512640 134672761 3221224544 3221223648 134560059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31260 30793 603 41 0 31219 0
vsize: 125040
[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 31061 0 0 0 118944 77 0 0 25 0 1 0 481369752 128851968 30993 4294967295 134512640 134672761 3221224544 3221223648 134560034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31458 30993 603 41 0 31417 0
vsize: 125832
[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14687
Raw data (stat): 14687 (minisat+) R 14686 7987 7986 0 -1 0 31061 0 0 0 119944 77 0 0 25 0 1 0 481369752 128851968 30993 4294967295 134512640 134672761 3221224544 3221223680 134560619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31458 30993 603 41 0 31417 0
vsize: 125832
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.16 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 14687
Raw data (stat): 14687 (minisat+) Z 14686 7987 7986 0 -1 12 31063 0 0 0 119944 83 0 0 25 0 1 0 481369752 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.16
CPU time (s): 1200.28
CPU user time (s): 1199.44
CPU system time (s): 0.836872
CPU usage (%): 100.01
Max. virtual memory (Kb): 125832
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####