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-fpga40_38_sat_pb.cnf.cr.opb
MD5SUM	69d239b72e8d1a72f9c55329043493e1
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	41
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	15.9626
Number of variables	2280
Total number of constraints	1636
Number of constraints which are clauses	1558
Number of constraints which are cardinality constraints (but not clauses)	78
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	20
Maximum length of a constraint	40
Trace number 5778

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-04-14 01:44:26 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4188 boxname=wulflinc20 idbench=52 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  69d239b72e8d1a72f9c55329043493e1  /oldhome/oroussel/tmp/wulflinc20/normalized-fpga40_38_sat_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc20/normalized-fpga40_38_sat_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc20/normalized-fpga40_38_sat_pb.cnf.cr.opb
IDLAUNCH: 4188
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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.215
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        885660 kB
Buffers:         35052 kB
Cached:          78116 kB
SwapCached:       2636 kB
Active:          49468 kB
Inactive:        69236 kB
HighTotal:      131008 kB
HighFree:        49056 kB
LowTotal:       903652 kB
LowFree:        836604 kB
SwapTotal:     2097892 kB
SwapFree:      2095256 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            24660 kB
Committed_AS:    63448 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 02:04:28 (client local time) WITH STATUS 0 IN 1200.24 SECONDS
stats: 4188 7 1200.24 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1636 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ......................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[  77]---> BDD-cost:   73
c ---[  76]---> BDD-cost:   73
c ---[  75]---> BDD-cost:   73
c ---[  74]---> BDD-cost:   73
c ---[  73]---> BDD-cost:   73
c ---[  72]---> BDD-cost:   73
c ---[  71]---> BDD-cost:   73
c ---[  70]---> BDD-cost:   73
c ---[  69]---> BDD-cost:   73
c ---[  68]---> BDD-cost:   73
c ---[  67]---> BDD-cost:   73
c ---[  66]---> BDD-cost:   73
c ---[  65]---> BDD-cost:   73
c ---[  64]---> BDD-cost:   73
c ---[  63]---> BDD-cost:   73
c ---[  62]---> BDD-cost:   73
c ---[  61]---> BDD-cost:   73
c ---[  60]---> BDD-cost:   73
c ---[  59]---> BDD-cost:   73
c ---[  58]---> BDD-cost:   73
c ---[  57]---> BDD-cost:   73
c ---[  56]---> BDD-cost:   73
c ---[  55]---> BDD-cost:   73
c ---[  54]---> BDD-cost:   73
c ---[  53]---> BDD-cost:   73
c ---[  52]---> BDD-cost:   73
c ---[  51]---> BDD-cost:   73
c ---[  50]---> BDD-cost:   73
c ---[  49]---> BDD-cost:   73
c ---[  48]---> BDD-cost:   73
c ---[  47]---> BDD-cost:   73
c ---[  46]---> BDD-cost:   73
c ---[  45]---> BDD-cost:   73
c ---[  44]---> BDD-cost:   73
c ---[  43]---> BDD-cost:   73
c ---[  42]---> BDD-cost:   73
c ---[  41]---> BDD-cost:   73
c ---[  40]---> BDD-cost:   73
c ---[  39]---> BDD-cost:   73
c ---[  38]---> BDD-cost:   73
c ---[  37]---> BDD-cost:   37
c ---[  36]---> BDD-cost:   37
c ---[  35]---> BDD-cost:   37
c ---[  34]---> BDD-cost:   37
c ---[  33]---> BDD-cost:   37
c ---[  32]---> BDD-cost:   37
c ---[  31]---> BDD-cost:   37
c ---[  30]---> BDD-cost:   37
c ---[  29]---> BDD-cost:   37
c ---[  28]---> BDD-cost:   37
c ---[  27]---> BDD-cost:   37
c ---[  26]---> BDD-cost:   37
c ---[  25]---> BDD-cost:   37
c ---[  24]---> BDD-cost:   37
c ---[  23]---> BDD-cost:   37
c ---[  22]---> BDD-cost:   37
c ---[  21]---> BDD-cost:   37
c ---[  20]---> BDD-cost:   37
c ---[  19]---> BDD-cost:   37
c ---[  18]---> BDD-cost:   37
c ---[  17]---> BDD-cost:   37
c ---[  16]---> BDD-cost:   37
c ---[  15]---> BDD-cost:   37
c ---[  14]---> BDD-cost:   37
c ---[  13]---> BDD-cost:   37
c ---[  12]---> BDD-cost:   37
c ---[  11]---> BDD-cost:   37
c ---[  10]---> BDD-cost:   37
c ---[   9]---> BDD-cost:   37
c ---[   8]---> BDD-cost:   37
c ---[   7]---> BDD-cost:   37
c ---[   6]---> BDD-cost:   37
c ---[   5]---> BDD-cost:   37
c ---[   4]---> BDD-cost:   37
c ---[   3]---> BDD-cost:   37
c ---[   2]---> BDD-cost:   37
c ---[   1]---> BDD-cost:   37
c ---[   0]---> BDD-cost:   37
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   12256    59766 |    4085       0        0     nan |  0.000 % |
c |       103 |   12256    59766 |    4493     103    23189   225.1 |  1.181 % |
c |       253 |   12256    59766 |    4942     253    33793   133.6 |  1.181 % |
c |       480 |   12256    59766 |    5437     480    75308   156.9 |  1.181 % |
c |       817 |   12256    59766 |    5980     817   169756   207.8 |  1.181 % |
c |      1323 |   12256    59766 |    6578    1323   266622   201.5 |  1.181 % |
c |      2082 |   12256    59766 |    7236    2082   346944   166.6 |  1.181 % |
c |      3221 |   12256    59766 |    7960    3221   672994   208.9 |  1.181 % |
c |      4933 |   12256    59766 |    8756    4933   891745   180.8 |  1.181 % |
c |      7495 |   12256    59766 |    9632    7495  1795103   239.5 |  1.181 % |
c |     11340 |   12256    59766 |   10595   11340  2331890   205.6 |  1.181 % |
c |     17107 |   12256    59766 |   11654   11437  3336088   291.7 |  1.181 % |
c |     25760 |   12256    59766 |   12820   12101  3971454   328.2 |  1.181 % |
c |     38736 |   12256    59766 |   14102   16761  4472808   266.9 |  1.181 % |
c |     58201 |   12256    59766 |   15512   18480  7868227   425.8 |  1.181 % |
c |     87394 |   12256    59766 |   17064   17668  2277590   128.9 |  1.181 % |
c |    131184 |   12256    59766 |   18770   21073  9678978   459.3 |  1.181 % |
c |    196873 |   12256    59766 |   20647   20482  7435518   363.0 |  1.181 % |
c |    295403 |   12256    59766 |   22712   24813  4118111   166.0 |  1.181 % |
#### 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.79 0.85 0.87 2/54 1361
Raw data (stat): 1361 (runsolver) R 1360 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480727525 1052672 99 4294967295 134512640 135381576 3221224416 3221219660 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.82 0.85 0.87 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 3013 0 0 0 991 8 0 0 25 0 1 0 480727525 13971456 2991 4294967295 134512640 134672761 3221224528 3221223664 134565054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3411 2991 603 41 0 3370 0
vsize: 13644
[startup+20.0011 s]
Raw data (loadavg): 0.85 0.86 0.87 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 3469 0 0 0 1990 9 0 0 25 0 1 0 480727525 15728640 3447 4294967295 134512640 134672761 3221224528 3221223696 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3840 3447 603 41 0 3799 0
vsize: 15360
[startup+30.0012 s]
Raw data (loadavg): 0.87 0.86 0.87 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 4921 0 0 0 2986 13 0 0 25 0 1 0 480727525 21803008 4899 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5323 4899 603 41 0 5282 0
vsize: 21292
[startup+40.0019 s]
Raw data (loadavg): 0.89 0.87 0.87 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 5951 0 0 0 3983 15 0 0 25 0 1 0 480727525 26001408 5929 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6348 5929 603 41 0 6307 0
vsize: 25392
[startup+50.0022 s]
Raw data (loadavg): 0.91 0.87 0.87 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 5954 0 0 0 4984 15 0 0 25 0 1 0 480727525 26001408 5932 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6348 5932 603 41 0 6307 0
vsize: 25392
[startup+60.0034 s]
Raw data (loadavg): 0.92 0.87 0.88 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 5955 0 0 0 5984 16 0 0 25 0 1 0 480727525 26001408 5933 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6348 5933 603 41 0 6307 0
vsize: 25392
[startup+70.0041 s]
Raw data (loadavg): 0.93 0.88 0.88 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 6726 0 0 0 6982 18 0 0 25 0 1 0 480727525 29265920 6704 4294967295 134512640 134672761 3221224528 3221223712 134559417 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7145 6704 603 41 0 7104 0
vsize: 28580
[startup+80.0048 s]
Raw data (loadavg): 0.94 0.88 0.88 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 6726 0 0 0 7981 18 0 0 25 0 1 0 480727525 29265920 6704 4294967295 134512640 134672761 3221224528 3221223632 134559866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7145 6704 603 41 0 7104 0
vsize: 28580
[startup+90.0055 s]
Raw data (loadavg): 0.95 0.89 0.88 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 6726 0 0 0 8982 18 0 0 25 0 1 0 480727525 29265920 6704 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7145 6704 603 41 0 7104 0
vsize: 28580
[startup+100.005 s]
Raw data (loadavg): 0.96 0.89 0.88 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 6752 0 0 0 9981 19 0 0 25 0 1 0 480727525 29265920 6730 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7145 6730 603 41 0 7104 0
vsize: 28580
[startup+110.006 s]
Raw data (loadavg): 0.96 0.89 0.88 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 7358 0 0 0 10980 20 0 0 25 0 1 0 480727525 31834112 7336 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7772 7336 603 41 0 7731 0
vsize: 31088
[startup+120.007 s]
Raw data (loadavg): 0.97 0.89 0.88 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 7358 0 0 0 11980 20 0 0 25 0 1 0 480727525 31834112 7336 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7772 7336 603 41 0 7731 0
vsize: 31088
[startup+130.006 s]
Raw data (loadavg): 0.97 0.90 0.88 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 7358 0 0 0 12980 20 0 0 25 0 1 0 480727525 31834112 7336 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7772 7336 603 41 0 7731 0
vsize: 31088
[startup+140.007 s]
Raw data (loadavg): 0.98 0.90 0.88 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 7358 0 0 0 13980 20 0 0 25 0 1 0 480727525 31834112 7336 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7772 7336 603 41 0 7731 0
vsize: 31088
[startup+150.008 s]
Raw data (loadavg): 0.98 0.90 0.88 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 7610 0 0 0 14980 21 0 0 25 0 1 0 480727525 32796672 7588 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8007 7588 603 41 0 7966 0
vsize: 32028
[startup+160.008 s]
Raw data (loadavg): 0.98 0.91 0.89 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 8213 0 0 0 15978 23 0 0 25 0 1 0 480727525 35373056 8191 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8636 8191 603 41 0 8595 0
vsize: 34544
[startup+170.008 s]
Raw data (loadavg): 0.98 0.91 0.89 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 8793 0 0 0 16976 25 0 0 25 0 1 0 480727525 37806080 8771 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9230 8771 603 41 0 9189 0
vsize: 36920
[startup+180.008 s]
Raw data (loadavg): 0.99 0.91 0.89 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 9413 0 0 0 17975 26 0 0 25 0 1 0 480727525 40267776 9391 4294967295 134512640 134672761 3221224528 3221223632 134560226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9831 9391 603 41 0 9790 0
vsize: 39324
[startup+190.008 s]
Raw data (loadavg): 0.99 0.91 0.89 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 9772 0 0 0 18973 28 0 0 25 0 1 0 480727525 41754624 9750 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10194 9750 603 41 0 10153 0
vsize: 40776
[startup+200.008 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 9774 0 0 0 19973 28 0 0 25 0 1 0 480727525 41725952 9752 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10187 9752 603 41 0 10146 0
vsize: 40748
[startup+210.009 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 9774 0 0 0 20974 28 0 0 25 0 1 0 480727525 41725952 9752 4294967295 134512640 134672761 3221224528 3221223696 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10187 9752 603 41 0 10146 0
vsize: 40748
[startup+220.01 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 9774 0 0 0 21974 28 0 0 25 0 1 0 480727525 41725952 9752 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10187 9752 603 41 0 10146 0
vsize: 40748
[startup+230.009 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 9774 0 0 0 22974 28 0 0 25 0 1 0 480727525 41725952 9752 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10187 9752 603 41 0 10146 0
vsize: 40748
[startup+240.009 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 9774 0 0 0 23974 28 0 0 25 0 1 0 480727525 41725952 9752 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10187 9752 603 41 0 10146 0
vsize: 40748
[startup+250.01 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 9774 0 0 0 24974 28 0 0 25 0 1 0 480727525 41725952 9752 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10187 9752 603 41 0 10146 0
vsize: 40748
[startup+260.011 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 9774 0 0 0 25974 28 0 0 25 0 1 0 480727525 41725952 9752 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10187 9752 603 41 0 10146 0
vsize: 40748
[startup+270.01 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 9774 0 0 0 26974 28 0 0 25 0 1 0 480727525 41725952 9752 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10187 9752 603 41 0 10146 0
vsize: 40748
[startup+280.01 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 9774 0 0 0 27974 28 0 0 25 0 1 0 480727525 41725952 9752 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10187 9752 603 41 0 10146 0
vsize: 40748
[startup+290.01 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 9774 0 0 0 28975 28 0 0 25 0 1 0 480727525 41725952 9752 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10187 9752 603 41 0 10146 0
vsize: 40748
[startup+300.01 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 9775 0 0 0 29975 29 0 0 25 0 1 0 480727525 41725952 9753 4294967295 134512640 134672761 3221224528 3221223712 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10187 9753 603 41 0 10146 0
vsize: 40748
[startup+310.011 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 9775 0 0 0 30975 29 0 0 25 0 1 0 480727525 41725952 9753 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10187 9753 603 41 0 10146 0
vsize: 40748
[startup+320.012 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 9775 0 0 0 31975 29 0 0 25 0 1 0 480727525 41725952 9753 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10187 9753 603 41 0 10146 0
vsize: 40748
[startup+330.012 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 9858 0 0 0 32975 29 0 0 25 0 1 0 480727525 42127360 9836 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10285 9836 603 41 0 10244 0
vsize: 41140
[startup+340.012 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 10225 0 0 0 33974 30 0 0 25 0 1 0 480727525 43626496 10203 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10651 10203 603 41 0 10610 0
vsize: 42604
[startup+350.013 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 10685 0 0 0 34973 31 0 0 25 0 1 0 480727525 45510656 10663 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11111 10663 603 41 0 11070 0
vsize: 44444
[startup+360.014 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 11157 0 0 0 35972 33 0 0 25 0 1 0 480727525 47542272 11135 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11607 11135 603 41 0 11566 0
vsize: 46428
[startup+370.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 11746 0 0 0 36971 34 0 0 25 0 1 0 480727525 49967104 11724 4294967295 134512640 134672761 3221224528 3221223632 134559805 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12199 11724 603 41 0 12158 0
vsize: 48796
[startup+380.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12153 0 0 0 37971 34 0 0 25 0 1 0 480727525 51654656 12131 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12611 12131 603 41 0 12570 0
vsize: 50444
[startup+390.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12398 0 0 0 38970 35 0 0 25 0 1 0 480727525 52731904 12376 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12874 12376 603 41 0 12833 0
vsize: 51496
[startup+400.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12398 0 0 0 39970 35 0 0 25 0 1 0 480727525 52731904 12376 4294967295 134512640 134672761 3221224528 3221223632 134559908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12874 12376 603 41 0 12833 0
vsize: 51496
[startup+410.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12398 0 0 0 40970 36 0 0 25 0 1 0 480727525 52731904 12376 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12874 12376 603 41 0 12833 0
vsize: 51496
[startup+420.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12398 0 0 0 41970 36 0 0 25 0 1 0 480727525 52731904 12376 4294967295 134512640 134672761 3221224528 3221223692 134559748 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12874 12376 603 41 0 12833 0
vsize: 51496
[startup+430.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12701 0 0 0 42969 36 0 0 25 0 1 0 480727525 53936128 12679 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13168 12679 603 41 0 13127 0
vsize: 52672
[startup+440.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12761 0 0 0 43969 37 0 0 25 0 1 0 480727525 54206464 12739 4294967295 134512640 134672761 3221224528 3221223632 134559902 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12739 603 41 0 13193 0
vsize: 52936
[startup+450.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12761 0 0 0 44969 37 0 0 25 0 1 0 480727525 54206464 12739 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12739 603 41 0 13193 0
vsize: 52936
[startup+460.017 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12761 0 0 0 45970 37 0 0 25 0 1 0 480727525 54206464 12739 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12739 603 41 0 13193 0
vsize: 52936
[startup+470.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12761 0 0 0 46970 37 0 0 25 0 1 0 480727525 54206464 12739 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12739 603 41 0 13193 0
vsize: 52936
[startup+480.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12781 0 0 0 47970 37 0 0 25 0 1 0 480727525 54206464 12759 4294967295 134512640 134672761 3221224528 3221223712 134559622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12759 603 41 0 13193 0
vsize: 52936
[startup+490.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12781 0 0 0 48970 37 0 0 25 0 1 0 480727525 54206464 12759 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12759 603 41 0 13193 0
vsize: 52936
[startup+500.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12781 0 0 0 49970 37 0 0 25 0 1 0 480727525 54206464 12759 4294967295 134512640 134672761 3221224528 3221223712 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12759 603 41 0 13193 0
vsize: 52936
[startup+510.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12781 0 0 0 50970 37 0 0 25 0 1 0 480727525 54206464 12759 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12759 603 41 0 13193 0
vsize: 52936
[startup+520.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12782 0 0 0 51970 37 0 0 25 0 1 0 480727525 54206464 12760 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12760 603 41 0 13193 0
vsize: 52936
[startup+530.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12782 0 0 0 52970 37 0 0 25 0 1 0 480727525 54206464 12760 4294967295 134512640 134672761 3221224528 3221223632 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12760 603 41 0 13193 0
vsize: 52936
[startup+540.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12782 0 0 0 53970 37 0 0 25 0 1 0 480727525 54206464 12760 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12760 603 41 0 13193 0
vsize: 52936
[startup+550.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12782 0 0 0 54971 37 0 0 25 0 1 0 480727525 54206464 12760 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12760 603 41 0 13193 0
vsize: 52936
[startup+560.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12782 0 0 0 55971 37 0 0 25 0 1 0 480727525 54206464 12760 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12760 603 41 0 13193 0
vsize: 52936
[startup+570.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12782 0 0 0 56971 38 0 0 25 0 1 0 480727525 54206464 12760 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12760 603 41 0 13193 0
vsize: 52936
[startup+580.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12782 0 0 0 57971 38 0 0 25 0 1 0 480727525 54206464 12760 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12760 603 41 0 13193 0
vsize: 52936
[startup+590.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12782 0 0 0 58971 38 0 0 25 0 1 0 480727525 54206464 12760 4294967295 134512640 134672761 3221224528 3221223632 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12760 603 41 0 13193 0
vsize: 52936
[startup+600.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12782 0 0 0 59971 38 0 0 25 0 1 0 480727525 54206464 12760 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12760 603 41 0 13193 0
vsize: 52936
[startup+610.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12782 0 0 0 60971 38 0 0 25 0 1 0 480727525 54206464 12760 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12760 603 41 0 13193 0
vsize: 52936
[startup+620.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12782 0 0 0 61971 38 0 0 25 0 1 0 480727525 54206464 12760 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12760 603 41 0 13193 0
vsize: 52936
[startup+630.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12782 0 0 0 62971 38 0 0 25 0 1 0 480727525 54206464 12760 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12760 603 41 0 13193 0
vsize: 52936
[startup+640.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12782 0 0 0 63972 38 0 0 25 0 1 0 480727525 54206464 12760 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12760 603 41 0 13193 0
vsize: 52936
[startup+650.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12782 0 0 0 64972 38 0 0 25 0 1 0 480727525 54206464 12760 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12760 603 41 0 13193 0
vsize: 52936
[startup+660.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12782 0 0 0 65972 38 0 0 25 0 1 0 480727525 54206464 12760 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12760 603 41 0 13193 0
vsize: 52936
[startup+670.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12782 0 0 0 66972 38 0 0 25 0 1 0 480727525 54206464 12760 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12760 603 41 0 13193 0
vsize: 52936
[startup+680.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12782 0 0 0 67972 39 0 0 25 0 1 0 480727525 54206464 12760 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12760 603 41 0 13193 0
vsize: 52936
[startup+690.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12782 0 0 0 68972 39 0 0 25 0 1 0 480727525 54206464 12760 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12760 603 41 0 13193 0
vsize: 52936
[startup+700.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12782 0 0 0 69972 39 0 0 25 0 1 0 480727525 54206464 12760 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12760 603 41 0 13193 0
vsize: 52936
[startup+710.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12782 0 0 0 70973 39 0 0 25 0 1 0 480727525 54206464 12760 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12760 603 41 0 13193 0
vsize: 52936
[startup+720.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12782 0 0 0 71973 39 0 0 25 0 1 0 480727525 54206464 12760 4294967295 134512640 134672761 3221224528 3221223632 134559981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12760 603 41 0 13193 0
vsize: 52936
[startup+730.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12782 0 0 0 72973 39 0 0 25 0 1 0 480727525 54206464 12760 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12760 603 41 0 13193 0
vsize: 52936
[startup+740.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12782 0 0 0 73973 39 0 0 25 0 1 0 480727525 54206464 12760 4294967295 134512640 134672761 3221224528 3221223696 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12760 603 41 0 13193 0
vsize: 52936
[startup+750.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12782 0 0 0 74973 39 0 0 25 0 1 0 480727525 54206464 12760 4294967295 134512640 134672761 3221224528 3221223696 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12760 603 41 0 13193 0
vsize: 52936
[startup+760.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12782 0 0 0 75973 39 0 0 25 0 1 0 480727525 54206464 12760 4294967295 134512640 134672761 3221224528 3221223632 134554636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12760 603 41 0 13193 0
vsize: 52936
[startup+770.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12782 0 0 0 76973 39 0 0 25 0 1 0 480727525 54206464 12760 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12760 603 41 0 13193 0
vsize: 52936
[startup+780.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12782 0 0 0 77973 39 0 0 25 0 1 0 480727525 54206464 12760 4294967295 134512640 134672761 3221224528 3221223632 134560492 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12760 603 41 0 13193 0
vsize: 52936
[startup+790.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12782 0 0 0 78973 39 0 0 25 0 1 0 480727525 54206464 12760 4294967295 134512640 134672761 3221224528 3221223632 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12760 603 41 0 13193 0
vsize: 52936
[startup+800.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12782 0 0 0 79973 40 0 0 25 0 1 0 480727525 54206464 12760 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12760 603 41 0 13193 0
vsize: 52936
[startup+810.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12784 0 0 0 80973 40 0 0 25 0 1 0 480727525 54206464 12762 4294967295 134512640 134672761 3221224528 3221223632 134559995 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12762 603 41 0 13193 0
vsize: 52936
[startup+820.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12784 0 0 0 81973 40 0 0 25 0 1 0 480727525 54206464 12762 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12762 603 41 0 13193 0
vsize: 52936
[startup+830.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12784 0 0 0 82973 40 0 0 25 0 1 0 480727525 54206464 12762 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12762 603 41 0 13193 0
vsize: 52936
[startup+840.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12785 0 0 0 83973 40 0 0 25 0 1 0 480727525 54206464 12763 4294967295 134512640 134672761 3221224528 3221223696 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12763 603 41 0 13193 0
vsize: 52936
[startup+850.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12785 0 0 0 84974 40 0 0 25 0 1 0 480727525 54206464 12763 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12763 603 41 0 13193 0
vsize: 52936
[startup+860.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12785 0 0 0 85974 40 0 0 25 0 1 0 480727525 54206464 12763 4294967295 134512640 134672761 3221224528 3221223696 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12763 603 41 0 13193 0
vsize: 52936
[startup+870.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12785 0 0 0 86974 40 0 0 25 0 1 0 480727525 54206464 12763 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12763 603 41 0 13193 0
vsize: 52936
[startup+880.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12785 0 0 0 87974 40 0 0 25 0 1 0 480727525 54206464 12763 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12763 603 41 0 13193 0
vsize: 52936
[startup+890.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12785 0 0 0 88974 40 0 0 25 0 1 0 480727525 54206464 12763 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12763 603 41 0 13193 0
vsize: 52936
[startup+900.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12785 0 0 0 89974 40 0 0 25 0 1 0 480727525 54206464 12763 4294967295 134512640 134672761 3221224528 3221223696 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12763 603 41 0 13193 0
vsize: 52936
[startup+910.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12785 0 0 0 90975 40 0 0 25 0 1 0 480727525 54206464 12763 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12763 603 41 0 13193 0
vsize: 52936
[startup+920.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12785 0 0 0 91975 40 0 0 25 0 1 0 480727525 54206464 12763 4294967295 134512640 134672761 3221224528 3221223696 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12763 603 41 0 13193 0
vsize: 52936
[startup+930.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1361
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12785 0 0 0 92975 40 0 0 25 0 1 0 480727525 54206464 12763 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12763 603 41 0 13193 0
vsize: 52936
[startup+940.024 s]
Raw data (loadavg): 1.07 0.99 0.91 2/57 1405
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12785 0 0 0 93974 40 0 0 25 0 1 0 480727525 54206464 12763 4294967295 134512640 134672761 3221224528 3221223696 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12763 603 41 0 13193 0
vsize: 52936
[startup+950.024 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 1414
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12785 0 0 0 94974 41 0 0 25 0 1 0 480727525 54206464 12763 4294967295 134512640 134672761 3221224528 3221223712 134558916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12763 603 41 0 13193 0
vsize: 52936
[startup+960.025 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 1414
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12785 0 0 0 95974 41 0 0 25 0 1 0 480727525 54206464 12763 4294967295 134512640 134672761 3221224528 3221223712 134559363 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12763 603 41 0 13193 0
vsize: 52936
[startup+970.025 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 1414
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12785 0 0 0 96974 41 0 0 25 0 1 0 480727525 54206464 12763 4294967295 134512640 134672761 3221224528 3221223712 134558664 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12763 603 41 0 13193 0
vsize: 52936
[startup+980.026 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 1414
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12785 0 0 0 97974 42 0 0 25 0 1 0 480727525 54206464 12763 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12763 603 41 0 13193 0
vsize: 52936
[startup+990.026 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 1414
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12785 0 0 0 98973 42 0 0 25 0 1 0 480727525 54206464 12763 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12763 603 41 0 13193 0
vsize: 52936
[startup+1000.03 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 1414
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12785 0 0 0 99973 43 0 0 25 0 1 0 480727525 54206464 12763 4294967295 134512640 134672761 3221224528 3221223696 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12763 603 41 0 13193 0
vsize: 52936
[startup+1010.03 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 1416
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12785 0 0 0 100973 43 0 0 25 0 1 0 480727525 54206464 12763 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12763 603 41 0 13193 0
vsize: 52936
[startup+1020.03 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 1416
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12785 0 0 0 101973 43 0 0 25 0 1 0 480727525 54206464 12763 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12763 603 41 0 13193 0
vsize: 52936
[startup+1030.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1416
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12785 0 0 0 102973 44 0 0 25 0 1 0 480727525 54206464 12763 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12763 603 41 0 13193 0
vsize: 52936
[startup+1040.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1416
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12785 0 0 0 103972 44 0 0 25 0 1 0 480727525 54206464 12763 4294967295 134512640 134672761 3221224528 3221223544 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12763 603 41 0 13193 0
vsize: 52936
[startup+1050.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1416
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12785 0 0 0 104972 45 0 0 25 0 1 0 480727525 54206464 12763 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12763 603 41 0 13193 0
vsize: 52936
[startup+1060.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1416
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12785 0 0 0 105972 45 0 0 25 0 1 0 480727525 54206464 12763 4294967295 134512640 134672761 3221224528 3221223712 134558859 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12763 603 41 0 13193 0
vsize: 52936
[startup+1070.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 1416
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12785 0 0 0 106972 45 0 0 25 0 1 0 480727525 54206464 12763 4294967295 134512640 134672761 3221224528 3221223632 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12763 603 41 0 13193 0
vsize: 52936
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1416
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12785 0 0 0 107972 45 0 0 25 0 1 0 480727525 54206464 12763 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12763 603 41 0 13193 0
vsize: 52936
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1416
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12786 0 0 0 108972 46 0 0 25 0 1 0 480727525 54206464 12764 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12764 603 41 0 13193 0
vsize: 52936
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1416
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12786 0 0 0 109971 46 0 0 25 0 1 0 480727525 54206464 12764 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12764 603 41 0 13193 0
vsize: 52936
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1416
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 12786 0 0 0 110971 46 0 0 25 0 1 0 480727525 54206464 12764 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13234 12764 603 41 0 13193 0
vsize: 52936
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1416
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 13374 0 0 0 111969 49 0 0 25 0 1 0 480727525 56750080 13352 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13855 13352 603 41 0 13814 0
vsize: 55420
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1416
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 13730 0 0 0 112968 50 0 0 25 0 1 0 480727525 58286080 13708 4294967295 134512640 134672761 3221224528 3221223632 134559998 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14230 13708 603 41 0 14189 0
vsize: 56920
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1416
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 13730 0 0 0 113968 50 0 0 25 0 1 0 480727525 58286080 13708 4294967295 134512640 134672761 3221224528 3221223712 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14230 13708 603 41 0 14189 0
vsize: 56920
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1416
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 13730 0 0 0 114968 50 0 0 25 0 1 0 480727525 58286080 13708 4294967295 134512640 134672761 3221224528 3221223664 134565064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14230 13708 603 41 0 14189 0
vsize: 56920
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1416
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 13730 0 0 0 115968 51 0 0 25 0 1 0 480727525 58286080 13708 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14230 13708 603 41 0 14189 0
vsize: 56920
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1416
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 13753 0 0 0 116967 51 0 0 25 0 1 0 480727525 58421248 13731 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14263 13731 603 41 0 14222 0
vsize: 57052
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1416
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 14421 0 0 0 117965 54 0 0 25 0 1 0 480727525 61149184 14399 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14929 14399 603 41 0 14888 0
vsize: 59716
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1416
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 15164 0 0 0 118963 56 0 0 25 0 1 0 480727525 64126976 15142 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15656 15142 603 41 0 15615 0
vsize: 62624
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1416
Raw data (stat): 1361 (minisat+) R 1360 27565 27564 0 -1 0 15620 0 0 0 119961 58 0 0 25 0 1 0 480727525 66048000 15598 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16125 15598 603 41 0 16084 0
vsize: 64500
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 1416
Raw data (stat): 1361 (minisat+) Z 1360 27565 27564 0 -1 12 15622 0 0 0 119961 61 0 0 25 0 1 0 480727525 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.06
CPU time (s): 1200.24
CPU user time (s): 1199.62
CPU system time (s): 0.616906
CPU usage (%): 100.015
Max. virtual memory (Kb): 64500
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####