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-chnl35_36_pb.cnf.cr.opb
MD5SUM	c779424bd1795a1e1adf6f4e7f38e307
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	37
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.075987
Number of variables	2520
Total number of constraints	142
Number of constraints which are clauses	72
Number of constraints which are cardinality constraints (but not clauses)	70
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	35
Maximum length of a constraint	36
Trace number 5334

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        890044 kB
Buffers:         34068 kB
Cached:          76988 kB
SwapCached:         56 kB
Active:          47652 kB
Inactive:        66356 kB
HighTotal:      131008 kB
HighFree:        50008 kB
LowTotal:       903652 kB
LowFree:        840036 kB
SwapTotal:     2097892 kB
SwapFree:      2097836 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7028 kB
Slab:            24924 kB
Committed_AS:    63704 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 23:53:07 (client local time) WITH STATUS 0 IN 1200.24 SECONDS
stats: 3774 7 1200.24 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 142 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................................................
c ---[  69]---> BDD-cost:   69
c ---[  68]---> BDD-cost:   69
c ---[  67]---> BDD-cost:   69
c ---[  66]---> BDD-cost:   69
c ---[  65]---> BDD-cost:   69
c ---[  64]---> BDD-cost:   69
c ---[  63]---> BDD-cost:   69
c ---[  62]---> BDD-cost:   69
c ---[  61]---> BDD-cost:   69
c ---[  60]---> BDD-cost:   69
c ---[  59]---> BDD-cost:   69
c ---[  58]---> BDD-cost:   69
c ---[  57]---> BDD-cost:   69
c ---[  56]---> BDD-cost:   69
c ---[  55]---> BDD-cost:   69
c ---[  54]---> BDD-cost:   69
c ---[  53]---> BDD-cost:   69
c ---[  52]---> BDD-cost:   69
c ---[  51]---> BDD-cost:   69
c ---[  50]---> BDD-cost:   69
c ---[  49]---> BDD-cost:   69
c ---[  48]---> BDD-cost:   69
c ---[  47]---> BDD-cost:   69
c ---[  46]---> BDD-cost:   69
c ---[  45]---> BDD-cost:   69
c ---[  44]---> BDD-cost:   69
c ---[  43]---> BDD-cost:   69
c ---[  42]---> BDD-cost:   69
c ---[  41]---> BDD-cost:   69
c ---[  40]---> BDD-cost:   69
c ---[  39]---> BDD-cost:   69
c ---[  38]---> BDD-cost:   69
c ---[  37]---> BDD-cost:   69
c ---[  36]---> BDD-cost:   69
c ---[  35]---> BDD-cost:   69
c ---[  34]---> BDD-cost:   69
c ---[  33]---> BDD-cost:   69
c ---[  32]---> BDD-cost:   69
c ---[  31]---> BDD-cost:   69
c ---[  30]---> BDD-cost:   69
c ---[  29]---> BDD-cost:   69
c ---[  28]---> BDD-cost:   69
c ---[  27]---> BDD-cost:   69
c ---[  26]---> BDD-cost:   69
c ---[  25]---> BDD-cost:   69
c ---[  24]---> BDD-cost:   69
c ---[  23]---> BDD-cost:   69
c ---[  22]---> BDD-cost:   69
c ---[  21]---> BDD-cost:   69
c ---[  20]---> BDD-cost:   69
c ---[  19]---> BDD-cost:   69
c ---[  18]---> BDD-cost:   69
c ---[  17]---> BDD-cost:   69
c ---[  16]---> BDD-cost:   69
c ---[  15]---> BDD-cost:   69
c ---[  14]---> BDD-cost:   69
c ---[  13]---> BDD-cost:   69
c ---[  12]---> BDD-cost:   69
c ---[  11]---> BDD-cost:   69
c ---[  10]---> BDD-cost:   69
c ---[   9]---> BDD-cost:   69
c ---[   8]---> BDD-cost:   69
c ---[   7]---> BDD-cost:   69
c ---[   6]---> BDD-cost:   69
c ---[   5]---> BDD-cost:   69
c ---[   4]---> BDD-cost:   69
c ---[   3]---> BDD-cost:   69
c ---[   2]---> BDD-cost:   69
c ---[   1]---> BDD-cost:   69
c ---[   0]---> BDD-cost:   69
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   12042    33670 |    3612       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/7280          
c   -- var.elim.:  2000/7280          
c   -- var.elim.:  3000/7280          
c   -- var.elim.:  4000/7280          
c   -- var.elim.:  5000/7280          
c   -- var.elim.:  6000/7280          
c   -- var.elim.:  7000/7280          
c   -- var.elim.:  7280/7280          
c   -- var.elim.:  1000/2812          
c   -- var.elim.:  2000/2812          
c   -- var.elim.:  2812/2812          
c   -- var.elim.:  146/146          
c   -- subsuming                       
c   -- var.elim.:  1000/1658          
c   -- var.elim.:  1658/1658          
c   -- var.elim.:  680/680          
c   -- var.elim.:  224/224          
c   -- var.elim.:  222/222          
c   -- var.elim.:  98/98          
c   -- var.elim.:  90/90          
c   -- var.elim.:  92/92          
c   -- var.elim.:  94/94          
c   -- var.elim.:  96/96          
c   -- var.elim.:  98/98          
c   -- var.elim.:  100/100          
c   -- var.elim.:  102/102          
c   -- var.elim.:  104/104          
c   -- var.elim.:  106/106          
c   -- var.elim.:  108/108          
c   -- var.elim.:  110/110          
c   -- var.elim.:  112/112          
c   -- var.elim.:  114/114          
c   -- var.elim.:#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.94 0.90 2/55 26990
Raw data (stat): 26990 (runsolver) R 26989 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479935311 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99965 s]
Raw data (loadavg): 0.87 0.94 0.90 2/55 26990
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 3605 0 0 0 988 11 0 0 25 0 1 0 479935311 16302080 3547 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3980 3547 603 41 0 3939 0
vsize: 15920
[startup+20.0007 s]
Raw data (loadavg): 0.89 0.94 0.90 2/55 26990
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 5158 0 0 0 1984 14 0 0 25 0 1 0 479935311 22581248 5100 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5513 5100 603 41 0 5472 0
vsize: 22052
[startup+30.0015 s]
Raw data (loadavg): 0.90 0.94 0.90 2/55 26990
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 5802 0 0 0 2982 16 0 0 25 0 1 0 479935311 25210880 5744 4294967295 134512640 134672761 3221224544 3221223640 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6155 5744 603 41 0 6114 0
vsize: 24620
[startup+40.0011 s]
Raw data (loadavg): 0.92 0.94 0.90 2/55 26990
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 5837 0 0 0 3982 17 0 0 25 0 1 0 479935311 25341952 5779 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6187 5779 603 41 0 6146 0
vsize: 24748
[startup+50.0021 s]
Raw data (loadavg): 0.93 0.94 0.90 2/55 26990
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 6177 0 0 0 4981 18 0 0 25 0 1 0 479935311 26750976 6119 4294967295 134512640 134672761 3221224544 3221223536 134565056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6531 6119 603 41 0 6490 0
vsize: 26124
[startup+60.0019 s]
Raw data (loadavg): 0.94 0.95 0.90 2/55 26990
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 6681 0 0 0 5980 19 0 0 25 0 1 0 479935311 29007872 6623 4294967295 134512640 134672761 3221224544 3221223640 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7082 6623 603 41 0 7041 0
vsize: 28328
[startup+70.0025 s]
Raw data (loadavg): 0.95 0.95 0.91 2/55 26990
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 6681 0 0 0 6980 19 0 0 25 0 1 0 479935311 28876800 6622 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7050 6622 603 41 0 7009 0
vsize: 28200
[startup+80.0026 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 26990
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 6911 0 0 0 7980 20 0 0 25 0 1 0 479935311 29814784 6851 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7279 6851 603 41 0 7238 0
vsize: 29116
[startup+90.0024 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 26990
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 6911 0 0 0 8980 20 0 0 25 0 1 0 479935311 29814784 6851 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7279 6851 603 41 0 7238 0
vsize: 29116
[startup+100.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 26990
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 7721 0 0 0 9978 22 0 0 25 0 1 0 479935311 33124352 7660 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8087 7660 603 41 0 8046 0
vsize: 32348
[startup+110.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 26990
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 7722 0 0 0 10978 22 0 0 25 0 1 0 479935311 33124352 7661 4294967295 134512640 134672761 3221224544 3221223728 134615722 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8087 7661 603 41 0 8046 0
vsize: 32348
[startup+120.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 26990
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 7722 0 0 0 11978 22 0 0 25 0 1 0 479935311 33124352 7661 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8087 7661 603 41 0 8046 0
vsize: 32348
[startup+130.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 26990
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 7793 0 0 0 12978 22 0 0 25 0 1 0 479935311 33390592 7732 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8152 7732 603 41 0 8111 0
vsize: 32608
[startup+140.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 26990
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 8378 0 0 0 13976 24 0 0 25 0 1 0 479935311 35811328 8316 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8743 8316 603 41 0 8702 0
vsize: 34972
[startup+150.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 26990
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 8578 0 0 0 14976 25 0 0 25 0 1 0 479935311 36605952 8516 4294967295 134512640 134672761 3221224544 3221223648 134604304 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8937 8516 603 41 0 8896 0
vsize: 35748
[startup+160.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26990
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 9055 0 0 0 15975 26 0 0 25 0 1 0 479935311 38608896 8992 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9426 8992 603 41 0 9385 0
vsize: 37704
[startup+170.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26990
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 9055 0 0 0 16975 26 0 0 25 0 1 0 479935311 38608896 8992 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9426 8992 603 41 0 9385 0
vsize: 37704
[startup+180.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26990
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 9690 0 0 0 17974 27 0 0 25 0 1 0 479935311 41193472 9627 4294967295 134512640 134672761 3221224544 3221223728 134615794 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10057 9627 603 41 0 10016 0
vsize: 40228
[startup+190.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26992
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 9690 0 0 0 18974 27 0 0 25 0 1 0 479935311 41193472 9627 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10057 9627 603 41 0 10016 0
vsize: 40228
[startup+200.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26992
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 9690 0 0 0 19974 27 0 0 25 0 1 0 479935311 41193472 9627 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10057 9627 603 41 0 10016 0
vsize: 40228
[startup+210.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26992
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 9690 0 0 0 20974 27 0 0 25 0 1 0 479935311 41193472 9627 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10057 9627 603 41 0 10016 0
vsize: 40228
[startup+220.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26992
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 9690 0 0 0 21974 27 0 0 25 0 1 0 479935311 41193472 9627 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10057 9627 603 41 0 10016 0
vsize: 40228
[startup+230.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26992
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 9690 0 0 0 22975 28 0 0 25 0 1 0 479935311 41193472 9627 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10057 9627 603 41 0 10016 0
vsize: 40228
[startup+240.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26992
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 9690 0 0 0 23974 28 0 0 25 0 1 0 479935311 41193472 9627 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10057 9627 603 41 0 10016 0
vsize: 40228
[startup+250.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26992
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 9690 0 0 0 24975 28 0 0 25 0 1 0 479935311 41193472 9627 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10057 9627 603 41 0 10016 0
vsize: 40228
[startup+260.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26992
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 9690 0 0 0 25975 28 0 0 25 0 1 0 479935311 41189376 9626 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10056 9626 603 41 0 10015 0
vsize: 40224
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26992
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 9690 0 0 0 26975 28 0 0 25 0 1 0 479935311 41189376 9626 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10056 9626 603 41 0 10015 0
vsize: 40224
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26992
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 9692 0 0 0 27975 28 0 0 25 0 1 0 479935311 41189376 9628 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10056 9628 603 41 0 10015 0
vsize: 40224
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26992
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 9692 0 0 0 28975 28 0 0 25 0 1 0 479935311 41189376 9628 4294967295 134512640 134672761 3221224544 3221223584 134612851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10056 9628 603 41 0 10015 0
vsize: 40224
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26992
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 9693 0 0 0 29975 28 0 0 25 0 1 0 479935311 41189376 9629 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10056 9629 603 41 0 10015 0
vsize: 40224
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26992
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 9693 0 0 0 30975 28 0 0 25 0 1 0 479935311 41189376 9629 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10056 9629 603 41 0 10015 0
vsize: 40224
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26992
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 9693 0 0 0 31976 28 0 0 25 0 1 0 479935311 41189376 9629 4294967295 134512640 134672761 3221224544 3221223728 134615526 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10056 9629 603 41 0 10015 0
vsize: 40224
[startup+330.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26992
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 9693 0 0 0 32976 28 0 0 25 0 1 0 479935311 41189376 9629 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10056 9629 603 41 0 10015 0
vsize: 40224
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26992
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 9693 0 0 0 33976 28 0 0 25 0 1 0 479935311 41189376 9629 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10056 9629 603 41 0 10015 0
vsize: 40224
[startup+350.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26992
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 9693 0 0 0 34976 28 0 0 25 0 1 0 479935311 41189376 9629 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10056 9629 603 41 0 10015 0
vsize: 40224
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26992
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 9693 0 0 0 35976 28 0 0 25 0 1 0 479935311 41189376 9629 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10056 9629 603 41 0 10015 0
vsize: 40224
[startup+370.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26992
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 9693 0 0 0 36976 29 0 0 25 0 1 0 479935311 41189376 9629 4294967295 134512640 134672761 3221224544 3221223584 134613761 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10056 9629 603 41 0 10015 0
vsize: 40224
[startup+380.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26992
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 9693 0 0 0 37976 29 0 0 25 0 1 0 479935311 41189376 9629 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10056 9629 603 41 0 10015 0
vsize: 40224
[startup+390.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26992
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 9693 0 0 0 38976 29 0 0 25 0 1 0 479935311 41181184 9629 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10054 9629 603 41 0 10013 0
vsize: 40216
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26992
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 9693 0 0 0 39977 29 0 0 25 0 1 0 479935311 41181184 9629 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10054 9629 603 41 0 10013 0
vsize: 40216
[startup+410.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26992
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 9694 0 0 0 40977 29 0 0 25 0 1 0 479935311 41181184 9630 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10054 9630 603 41 0 10013 0
vsize: 40216
[startup+420.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26992
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 9694 0 0 0 41977 29 0 0 25 0 1 0 479935311 41181184 9630 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10054 9630 603 41 0 10013 0
vsize: 40216
[startup+430.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26992
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 9694 0 0 0 42977 29 0 0 25 0 1 0 479935311 41181184 9630 4294967295 134512640 134672761 3221224544 3221223584 134612871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10054 9630 603 41 0 10013 0
vsize: 40216
[startup+440.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26992
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 9694 0 0 0 43977 29 0 0 25 0 1 0 479935311 41181184 9630 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10054 9630 603 41 0 10013 0
vsize: 40216
[startup+450.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26992
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 10677 0 0 0 44974 32 0 0 25 0 1 0 479935311 45191168 10613 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11033 10613 603 41 0 10992 0
vsize: 44132
[startup+460.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26992
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 11809 0 0 0 45971 36 0 0 25 0 1 0 479935311 49975296 11745 4294967295 134512640 134672761 3221224544 3221223640 134616347 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12201 11745 603 41 0 12160 0
vsize: 48804
[startup+470.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26992
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 11811 0 0 0 46971 36 0 0 25 0 1 0 479935311 49844224 11746 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12169 11746 603 41 0 12128 0
vsize: 48676
[startup+480.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26992
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 11813 0 0 0 47971 36 0 0 25 0 1 0 479935311 49844224 11748 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12169 11748 603 41 0 12128 0
vsize: 48676
[startup+490.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26994
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 11814 0 0 0 48971 36 0 0 25 0 1 0 479935311 49844224 11749 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12169 11749 603 41 0 12128 0
vsize: 48676
[startup+500.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26994
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 11824 0 0 0 49972 36 0 0 25 0 1 0 479935311 49975296 11759 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12201 11759 603 41 0 12160 0
vsize: 48804
[startup+510.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26994
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 12500 0 0 0 50970 37 0 0 25 0 1 0 479935311 52674560 12435 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12860 12435 603 41 0 12819 0
vsize: 51440
[startup+520.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26994
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 13309 0 0 0 51969 39 0 0 25 0 1 0 479935311 55980032 13244 4294967295 134512640 134672761 3221224544 3221223584 134612696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13667 13244 603 41 0 13626 0
vsize: 54668
[startup+530.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26994
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 14009 0 0 0 52967 41 0 0 25 0 1 0 479935311 58859520 13944 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14370 13944 603 41 0 14329 0
vsize: 57480
[startup+540.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26994
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 14009 0 0 0 53967 41 0 0 25 0 1 0 479935311 58859520 13944 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14370 13944 603 41 0 14329 0
vsize: 57480
[startup+550.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26994
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 14009 0 0 0 54967 41 0 0 25 0 1 0 479935311 58859520 13944 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14370 13944 603 41 0 14329 0
vsize: 57480
[startup+560.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26994
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 14009 0 0 0 55967 41 0 0 25 0 1 0 479935311 58859520 13944 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14370 13944 603 41 0 14329 0
vsize: 57480
[startup+570.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26994
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 14009 0 0 0 56968 41 0 0 25 0 1 0 479935311 58859520 13944 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14370 13944 603 41 0 14329 0
vsize: 57480
[startup+580.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26994
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 14010 0 0 0 57967 41 0 0 25 0 1 0 479935311 58859520 13945 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14370 13945 603 41 0 14329 0
vsize: 57480
[startup+590.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26994
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 14010 0 0 0 58968 41 0 0 25 0 1 0 479935311 58859520 13945 4294967295 134512640 134672761 3221224544 3221223728 134615526 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14370 13945 603 41 0 14329 0
vsize: 57480
[startup+600.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26994
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 14133 0 0 0 59967 42 0 0 25 0 1 0 479935311 59396096 14068 4294967295 134512640 134672761 3221224544 3221223600 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14501 14068 603 41 0 14460 0
vsize: 58004
[startup+610.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26994
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 14133 0 0 0 60967 42 0 0 25 0 1 0 479935311 59363328 14068 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14493 14068 603 41 0 14452 0
vsize: 57972
[startup+620.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26994
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 14133 0 0 0 61967 42 0 0 25 0 1 0 479935311 59363328 14068 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14493 14068 603 41 0 14452 0
vsize: 57972
[startup+630.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26994
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 14133 0 0 0 62968 42 0 0 25 0 1 0 479935311 59363328 14068 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14493 14068 603 41 0 14452 0
vsize: 57972
[startup+640.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26994
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 14133 0 0 0 63968 42 0 0 25 0 1 0 479935311 59363328 14068 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14493 14068 603 41 0 14452 0
vsize: 57972
[startup+650.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26994
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 14133 0 0 0 64968 42 0 0 25 0 1 0 479935311 59363328 14068 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14493 14068 603 41 0 14452 0
vsize: 57972
[startup+660.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26994
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 14133 0 0 0 65968 42 0 0 25 0 1 0 479935311 59363328 14068 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14493 14068 603 41 0 14452 0
vsize: 57972
[startup+670.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26994
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 14133 0 0 0 66968 42 0 0 25 0 1 0 479935311 59363328 14068 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14493 14068 603 41 0 14452 0
vsize: 57972
[startup+680.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26994
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 14774 0 0 0 67966 44 0 0 25 0 1 0 479935311 62050304 14709 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15149 14709 603 41 0 15108 0
vsize: 60596
[startup+690.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26994
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 14911 0 0 0 68966 44 0 0 25 0 1 0 479935311 62550016 14846 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15271 14846 603 41 0 15230 0
vsize: 61084
[startup+700.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26994
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 14911 0 0 0 69966 44 0 0 25 0 1 0 479935311 62550016 14846 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15271 14846 603 41 0 15230 0
vsize: 61084
[startup+710.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26994
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 14911 0 0 0 70967 44 0 0 25 0 1 0 479935311 62550016 14846 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15271 14846 603 41 0 15230 0
vsize: 61084
[startup+720.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26994
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 14911 0 0 0 71967 44 0 0 25 0 1 0 479935311 62550016 14846 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15271 14846 603 41 0 15230 0
vsize: 61084
[startup+730.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26994
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15045 0 0 0 72967 45 0 0 25 0 1 0 479935311 63090688 14979 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15403 14979 603 41 0 15362 0
vsize: 61612
[startup+740.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26994
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15045 0 0 0 73967 45 0 0 25 0 1 0 479935311 63090688 14979 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15403 14979 603 41 0 15362 0
vsize: 61612
[startup+750.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26994
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15045 0 0 0 74967 45 0 0 25 0 1 0 479935311 63090688 14979 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15403 14979 603 41 0 15362 0
vsize: 61612
[startup+760.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26994
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 75967 45 0 0 25 0 1 0 479935311 63090688 14981 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15403 14981 603 41 0 15362 0
vsize: 61612
[startup+770.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26994
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 76967 45 0 0 25 0 1 0 479935311 63078400 14980 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15400 14980 603 41 0 15359 0
vsize: 61600
[startup+780.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26994
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 77968 45 0 0 25 0 1 0 479935311 63078400 14980 4294967295 134512640 134672761 3221224544 3221223584 134603562 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15400 14980 603 41 0 15359 0
vsize: 61600
[startup+790.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26996
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 78968 45 0 0 25 0 1 0 479935311 63078400 14980 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15400 14980 603 41 0 15359 0
vsize: 61600
[startup+800.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26996
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 79968 45 0 0 25 0 1 0 479935311 63078400 14980 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15400 14980 603 41 0 15359 0
vsize: 61600
[startup+810.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26996
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 80968 45 0 0 25 0 1 0 479935311 63078400 14980 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15400 14980 603 41 0 15359 0
vsize: 61600
[startup+820.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26996
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 81968 45 0 0 25 0 1 0 479935311 63078400 14980 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15400 14980 603 41 0 15359 0
vsize: 61600
[startup+830.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26996
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 82968 45 0 0 25 0 1 0 479935311 63078400 14980 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15400 14980 603 41 0 15359 0
vsize: 61600
[startup+840.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26996
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 83969 45 0 0 25 0 1 0 479935311 63078400 14980 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15400 14980 603 41 0 15359 0
vsize: 61600
[startup+850.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26996
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 84969 45 0 0 25 0 1 0 479935311 63078400 14980 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15400 14980 603 41 0 15359 0
vsize: 61600
[startup+860.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26996
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 85968 45 0 0 25 0 1 0 479935311 63078400 14980 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15400 14980 603 41 0 15359 0
vsize: 61600
[startup+870.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26996
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 86969 45 0 0 25 0 1 0 479935311 63078400 14980 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15400 14980 603 41 0 15359 0
vsize: 61600
[startup+880.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26996
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 87969 45 0 0 25 0 1 0 479935311 63078400 14980 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15400 14980 603 41 0 15359 0
vsize: 61600
[startup+890.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26996
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 88969 45 0 0 25 0 1 0 479935311 63078400 14980 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15400 14980 603 41 0 15359 0
vsize: 61600
[startup+900.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26996
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 89969 45 0 0 25 0 1 0 479935311 63074304 14980 4294967295 134512640 134672761 3221224544 3221223584 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15399 14980 603 41 0 15358 0
vsize: 61596
[startup+910.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26996
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 90969 45 0 0 25 0 1 0 479935311 63074304 14980 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15399 14980 603 41 0 15358 0
vsize: 61596
[startup+920.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26996
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 91969 45 0 0 25 0 1 0 479935311 63074304 14980 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15399 14980 603 41 0 15358 0
vsize: 61596
[startup+930.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26996
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 92969 45 0 0 25 0 1 0 479935311 63074304 14980 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15399 14980 603 41 0 15358 0
vsize: 61596
[startup+940.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26996
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 93970 45 0 0 25 0 1 0 479935311 63074304 14980 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15399 14980 603 41 0 15358 0
vsize: 61596
[startup+950.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26996
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 94970 45 0 0 25 0 1 0 479935311 63074304 14980 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15399 14980 603 41 0 15358 0
vsize: 61596
[startup+960.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26996
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 95970 46 0 0 25 0 1 0 479935311 63074304 14980 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15399 14980 603 41 0 15358 0
vsize: 61596
[startup+970.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26996
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 96970 46 0 0 25 0 1 0 479935311 63074304 14980 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15399 14980 603 41 0 15358 0
vsize: 61596
[startup+980.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26996
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 97970 46 0 0 25 0 1 0 479935311 63074304 14980 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15399 14980 603 41 0 15358 0
vsize: 61596
[startup+990.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26996
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 98970 46 0 0 25 0 1 0 479935311 63074304 14980 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15399 14980 603 41 0 15358 0
vsize: 61596
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26996
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 99970 46 0 0 25 0 1 0 479935311 63074304 14980 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15399 14980 603 41 0 15358 0
vsize: 61596
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26996
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 100970 46 0 0 25 0 1 0 479935311 63074304 14980 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15399 14980 603 41 0 15358 0
vsize: 61596
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26996
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 101971 46 0 0 25 0 1 0 479935311 63074304 14980 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15399 14980 603 41 0 15358 0
vsize: 61596
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26996
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 102971 46 0 0 25 0 1 0 479935311 63074304 14980 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15399 14980 603 41 0 15358 0
vsize: 61596
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26996
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 103971 46 0 0 25 0 1 0 479935311 63074304 14980 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15399 14980 603 41 0 15358 0
vsize: 61596
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26996
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 104971 46 0 0 25 0 1 0 479935311 63074304 14980 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15399 14980 603 41 0 15358 0
vsize: 61596
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26996
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 105971 46 0 0 25 0 1 0 479935311 63074304 14980 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15399 14980 603 41 0 15358 0
vsize: 61596
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26996
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 106971 46 0 0 25 0 1 0 479935311 63074304 14980 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15399 14980 603 41 0 15358 0
vsize: 61596
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26996
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 107971 46 0 0 25 0 1 0 479935311 63074304 14980 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15399 14980 603 41 0 15358 0
vsize: 61596
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26998
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 108972 46 0 0 25 0 1 0 479935311 63074304 14980 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15399 14980 603 41 0 15358 0
vsize: 61596
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26998
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 109972 46 0 0 25 0 1 0 479935311 63074304 14980 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15399 14980 603 41 0 15358 0
vsize: 61596
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26998
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 110972 46 0 0 25 0 1 0 479935311 63074304 14980 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15399 14980 603 41 0 15358 0
vsize: 61596
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26998
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 111972 47 0 0 25 0 1 0 479935311 63074304 14980 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15399 14980 603 41 0 15358 0
vsize: 61596
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26998
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 112972 47 0 0 25 0 1 0 479935311 63074304 14980 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15399 14980 603 41 0 15358 0
vsize: 61596
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26998
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 113972 47 0 0 25 0 1 0 479935311 63074304 14980 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15399 14980 603 41 0 15358 0
vsize: 61596
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26998
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 114972 47 0 0 25 0 1 0 479935311 63074304 14980 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15399 14980 603 41 0 15358 0
vsize: 61596
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26998
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 115972 47 0 0 25 0 1 0 479935311 63074304 14980 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15399 14980 603 41 0 15358 0
vsize: 61596
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26998
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 116973 47 0 0 25 0 1 0 479935311 63074304 14980 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15399 14980 603 41 0 15358 0
vsize: 61596
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26998
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 117973 47 0 0 25 0 1 0 479935311 63074304 14980 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15399 14980 603 41 0 15358 0
vsize: 61596
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26998
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 118973 47 0 0 25 0 1 0 479935311 63074304 14980 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15399 14980 603 41 0 15358 0
vsize: 61596
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26998
Raw data (stat): 26990 (minisat+) R 26989 22929 22928 0 -1 0 15047 0 0 0 119973 47 0 0 25 0 1 0 479935311 63074304 14980 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15399 14980 603 41 0 15358 0
vsize: 61596
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 26998
Raw data (stat): 26990 (minisat+) Z 26989 22929 22928 0 -1 12 15047 0 0 0 119973 50 0 0 25 0 1 0 479935311 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

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