PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl50_60_pb.cnf.cr.opb
MD5SUM	6968a43b42bba7df68b13fdfd3b616a1
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	61
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.187971
Number of variables	6000
Total number of constraints	220
Number of constraints which are clauses	120
Number of constraints which are cardinality constraints (but not clauses)	100
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	50
Maximum length of a constraint	60
Trace number 5388

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        907712 kB
Buffers:         34824 kB
Cached:          72616 kB
SwapCached:          0 kB
Active:          53600 kB
Inactive:        56700 kB
HighTotal:      131008 kB
HighFree:        54544 kB
LowTotal:       903652 kB
LowFree:        853168 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            10984 kB
Committed_AS:    71656 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 23:57:00 (client local time) WITH STATUS 0 IN 1200.3 SECONDS
stats: 3782 7 1200.3 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 220 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................................................................................................
c ---[  99]---> BDD-cost:  117
c ---[  98]---> BDD-cost:  117
c ---[  97]---> BDD-cost:  117
c ---[  96]---> BDD-cost:  117
c ---[  95]---> BDD-cost:  117
c ---[  94]---> BDD-cost:  117
c ---[  93]---> BDD-cost:  117
c ---[  92]---> BDD-cost:  117
c ---[  91]---> BDD-cost:  117
c ---[  90]---> BDD-cost:  117
c ---[  89]---> BDD-cost:  117
c ---[  88]---> BDD-cost:  117
c ---[  87]---> BDD-cost:  117
c ---[  86]---> BDD-cost:  117
c ---[  85]---> BDD-cost:  117
c ---[  84]---> BDD-cost:  117
c ---[  83]---> BDD-cost:  117
c ---[  82]---> BDD-cost:  117
c ---[  81]---> BDD-cost:  117
c ---[  80]---> BDD-cost:  117
c ---[  79]---> BDD-cost:  117
c ---[  78]---> BDD-cost:  117
c ---[  77]---> BDD-cost:  117
c ---[  76]---> BDD-cost:  117
c ---[  75]---> BDD-cost:  117
c ---[  74]---> BDD-cost:  117
c ---[  73]---> BDD-cost:  117
c ---[  72]---> BDD-cost:  117
c ---[  71]---> BDD-cost:  117
c ---[  70]---> BDD-cost:  117
c ---[  69]---> BDD-cost:  117
c ---[  68]---> BDD-cost:  117
c ---[  67]---> BDD-cost:  117
c ---[  66]---> BDD-cost:  117
c ---[  65]---> BDD-cost:  117
c ---[  64]---> BDD-cost:  117
c ---[  63]---> BDD-cost:  117
c ---[  62]---> BDD-cost:  117
c ---[  61]---> BDD-cost:  117
c ---[  60]---> BDD-cost:  117
c ---[  59]---> BDD-cost:  117
c ---[  58]---> BDD-cost:  117
c ---[  57]---> BDD-cost:  117
c ---[  56]---> BDD-cost:  117
c ---[  55]---> BDD-cost:  117
c ---[  54]---> BDD-cost:  117
c ---[  53]---> BDD-cost:  117
c ---[  52]---> BDD-cost:  117
c ---[  51]---> BDD-cost:  117
c ---[  50]---> BDD-cost:  117
c ---[  49]---> BDD-cost:  117
c ---[  48]---> BDD-cost:  117
c ---[  47]---> BDD-cost:  117
c ---[  46]---> BDD-cost:  117
c ---[  45]---> BDD-cost:  117
c ---[  44]---> BDD-cost:  117
c ---[  43]---> BDD-cost:  117
c ---[  42]---> BDD-cost:  117
c ---[  41]---> BDD-cost:  117
c ---[  40]---> BDD-cost:  117
c ---[  39]---> BDD-cost:  117
c ---[  38]---> BDD-cost:  117
c ---[  37]---> BDD-cost:  117
c ---[  36]---> BDD-cost:  117
c ---[  35]---> BDD-cost:  117
c ---[  34]---> BDD-cost:  117
c ---[  33]---> BDD-cost:  117
c ---[  32]---> BDD-cost:  117
c ---[  31]---> BDD-cost:  117
c ---[  30]---> BDD-cost:  117
c ---[  29]---> BDD-cost:  117
c ---[  28]---> BDD-cost:  117
c ---[  27]---> BDD-cost:  117
c ---[  26]---> BDD-cost:  117
c ---[  25]---> BDD-cost:  117
c ---[  24]---> BDD-cost:  117
c ---[  23]---> BDD-cost:  117
c ---[  22]---> BDD-cost:  117
c ---[  21]---> BDD-cost:  117
c ---[  20]---> BDD-cost:  117
c ---[  19]---> BDD-cost:  117
c ---[  18]---> BDD-cost:  117
c ---[  17]---> BDD-cost:  117
c ---[  16]---> BDD-cost:  117
c ---[  15]---> BDD-cost:  117
c ---[  14]---> BDD-cost:  117
c ---[  13]---> BDD-cost:  117
c ---[  12]---> BDD-cost:  117
c ---[  11]---> BDD-cost:  117
c ---[  10]---> BDD-cost:  117
c ---[   9]---> BDD-cost:  117
c ---[   8]---> BDD-cost:  117
c ---[   7]---> BDD-cost:  117
c ---[   6]---> BDD-cost:  117
c ---[   5]---> BDD-cost:  117
c ---[   4]---> BDD-cost:  117
c ---[   3]---> BDD-cost:  117
c ---[   2]---> BDD-cost:  117
c ---[   1]---> BDD-cost:  117
c ---[   0]---> BDD-cost:  117
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   29220    81700 |    8765       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/17600          
c   -- var.elim.:  2000/17600          
c   -- var.elim.:  3000/17600          
c   -- var.elim.:  4000/17600          
c   -- var.elim.:  5000/17600          
c   -- var.elim.:  6000/17600          
c   -- var.elim.:  7000/17600          
c   -- var.elim.:  8000/17600          
c   -- var.elim.:  9000/17600          
c   -- var.elim.:  10000/17600          
c   -- var.elim.:  11000/17600          
c   -- var.elim.:  12000/17600          
c   -- var.elim.:  13000/17600          
c   -- var.elim.:  14000/17600          
c   -- var.elim.:  15000/17600          
c   -- var.elim.:  16000/17600          
c   -- var.elim.:  17000/17600          
c   -- var.elim.:  17600/17600          
c   -- var.elim.:  1000/6436          
c   -- var.elim.:  2000/6436          
c   -- var.elim.:  3000/6436          
c   -- var.elim.:  4000/6436          
c   -- var.elim.:  5000/6436          
c   -- var.elim.:  6000/6436          
c   -- var.elim.:  6436/6436          
c   -- var.elim.:  206/206          
c   -- subsuming                       
c   -- var.elim.:  1000/3596          
c   -- var.elim.:  2000/3596          
c   -- var.elim.:  3000/3596          
c   -- var.elim.:  3596/3596          
c   -- var.elim.:  982/982          
c   -- var.elim.:  124/124          
c   -- var.elim.:  116/116          
c   -- var.elim.:  118/118          
c   -- var.elim.:  120/120          
c   -- var.elim.:  122/122          
c   -- var.elim.:  124/124          
c   -- var.elim.:  126/126          
c   -- var.elim.:  128/128          
c   -- var.elim.:  130/130          
c   -- var.elim.:  132/132          
c   -- var.elim.:  134/134          
c   -- var.elim.:  136/136          
c   -- var.elim.:  138/138          
c   -- var.elim.:  140/140          
c   -- var.elim.:  142/142          
c   -- var.elim.:  144/144          
c   -- var.elim.:  146/146          
c   -- var.elim.:  148/148          
c   -- var.elim.:  150/150          
c   -- var.elim.:  152/152          
c   -- var.elim.:  154/154          
c   -- var.elim.:  156/156          
c   -- var.elim.:  158/158          
c   -- var.elim.:  160/160          
c   -- var.elim.:  162/162          
c   -- var.elim.:  164/164          
c   -- var.elim.:  166/166          
c   -- var.elim.:  168/168          
c   -- var.elim.:  170/170          
c   -- var.elim.:  172/172          
c   -- var.elim.:  174/174          
c   -- var.elim.:  176/176          
c   -- var.elim.:  178/178          
c   -- var.elim.:  180/180          
c   -- var.elim.:  182/182          
c   -- var.elim.:  184/184          
c   -- var.elim.:  186/186          
c   -- var.elim.:  188/188          
c   -- var.elim.:  190/190          
c   -- var.elim.:  192/192          
c   -- var.elim.:  194/194          
c   -- var.elim.:  196/196          
c   -- var.elim.:  198/198          
c   -- var.elim.:  200/200          
c   -- var.elim.:  202/202          
c   -- var.elim.:  204/204          
c   -- var.elim.:  206/206          
c   -- var.elim.:  208/208          
c   -- var.elim.:  210/210          
c   -- var.elim.:  212/212          
c   -- var.elim.:  214/214          
c   -- var.elim.:  216/216          
c   -- var.elim.:  218/218          
c   -- var.elim.:  506/506          
c   -- subsuming                       
c   -- var.elim.:  1000/6326          
c   -- var.elim.:  2000/6326          
c   -- var.elim.:  3000/6326          
c   -- var.elim.:  4000/6326          
c   -- var.elim.:  5000/6326          
c   -- var.elim.:  6000/6326          
c   -- var.elim.:  6326/6326          
c   -- var.elim.:  1000/6078          
c   -- var.elim.:  2000/6078          
c   -- var.elim.:  3000/6078          
c   -- var.elim.:  4000/6078          
c   -- var.elim.:  5000/6078          
c   -- var.elim.:  6000/6078          
c   -- var.elim.:  6078/6078          
c   -- var.elim.:  414/414          
c   -- subsuming                       
c   -- var.elim.:  784/784          
c |         0 |   27938   102382 |      --       0       --      -- |     --   | -1282/20982
c |         0 |   27938   102382 |   11175       0        0     nan |  0.000 % |
c |       101 |   27938   102382 |   12292     101    18681   185.0 |  0.598 % |
c |       252 |   27938   102382 |   13521     252    46231   183.5 |  0.598 % |
c |       480 |   27938   1023#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.94 0.90 2/54 10159
Raw data (stat): 10159 (runsolver) R 10158 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421738164 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 4343 0 0 0 987 12 0 0 25 0 1 0 421738164 19906560 4132 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4860 4132 603 41 0 4819 0
vsize: 19440
[startup+20.0013 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 6139 0 0 0 1981 17 0 0 25 0 1 0 421738164 27303936 5928 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6666 5928 603 41 0 6625 0
vsize: 26664
[startup+30.0016 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 7982 0 0 0 2977 22 0 0 25 0 1 0 421738164 34836480 7771 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8505 7771 603 41 0 8464 0
vsize: 34020
[startup+40.0018 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 9076 0 0 0 3974 25 0 0 25 0 1 0 421738164 39317504 8865 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9599 8865 603 41 0 9558 0
vsize: 38396
[startup+50.0027 s]
Raw data (loadavg): 1.01 0.96 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 10522 0 0 0 4971 28 0 0 25 0 1 0 421738164 45264896 10311 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11051 10311 603 41 0 11010 0
vsize: 44204
[startup+60.0022 s]
Raw data (loadavg): 1.01 0.96 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 11781 0 0 0 5968 31 0 0 25 0 1 0 421738164 50434048 11570 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12313 11570 603 41 0 12272 0
vsize: 49252
[startup+70.0034 s]
Raw data (loadavg): 1.01 0.96 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 12635 0 0 0 6965 34 0 0 25 0 1 0 421738164 53862400 12424 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13150 12424 603 41 0 13109 0
vsize: 52600
[startup+80.0042 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 14282 0 0 0 7962 37 0 0 25 0 1 0 421738164 60604416 14071 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14796 14071 603 41 0 14755 0
vsize: 59184
[startup+90.0038 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 15690 0 0 0 8960 40 0 0 25 0 1 0 421738164 66428928 15479 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16218 15479 603 41 0 16177 0
vsize: 64872
[startup+100.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 17347 0 0 0 9956 43 0 0 25 0 1 0 421738164 73359360 17136 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17910 17137 603 41 0 17869 0
vsize: 71640
[startup+110.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 18982 0 0 0 10953 47 0 0 25 0 1 0 421738164 79970304 18771 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19524 18771 603 41 0 19483 0
vsize: 78096
[startup+120.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 19586 0 0 0 11951 49 0 0 25 0 1 0 421738164 82374656 19367 4294967295 134512640 134672761 3221224544 3221223648 134604316 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20111 19367 603 41 0 20070 0
vsize: 80444
[startup+130.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 19586 0 0 0 12951 49 0 0 25 0 1 0 421738164 82374656 19367 4294967295 134512640 134672761 3221224544 3221223584 134613748 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20111 19367 603 41 0 20070 0
vsize: 80444
[startup+140.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 19586 0 0 0 13951 49 0 0 25 0 1 0 421738164 82374656 19367 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20111 19367 603 41 0 20070 0
vsize: 80444
[startup+150.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 19586 0 0 0 14951 49 0 0 25 0 1 0 421738164 82374656 19367 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20111 19367 603 41 0 20070 0
vsize: 80444
[startup+160.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 19586 0 0 0 15952 49 0 0 25 0 1 0 421738164 82374656 19367 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20111 19367 603 41 0 20070 0
vsize: 80444
[startup+170.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 19586 0 0 0 16952 49 0 0 25 0 1 0 421738164 82374656 19367 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20111 19367 603 41 0 20070 0
vsize: 80444
[startup+180.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 19586 0 0 0 17952 49 0 0 25 0 1 0 421738164 82374656 19367 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20111 19367 603 41 0 20070 0
vsize: 80444
[startup+190.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 19586 0 0 0 18952 49 0 0 25 0 1 0 421738164 82374656 19367 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20111 19367 603 41 0 20070 0
vsize: 80444
[startup+200.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 19586 0 0 0 19952 49 0 0 25 0 1 0 421738164 82374656 19367 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20111 19367 603 41 0 20070 0
vsize: 80444
[startup+210.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 19833 0 0 0 20952 50 0 0 25 0 1 0 421738164 83427328 19614 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20368 19614 603 41 0 20327 0
vsize: 81472
[startup+220.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 20565 0 0 0 21951 51 0 0 25 0 1 0 421738164 86441984 20346 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21104 20346 603 41 0 21063 0
vsize: 84416
[startup+230.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 20977 0 0 0 22950 52 0 0 25 0 1 0 421738164 88174592 20758 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21527 20758 603 41 0 21486 0
vsize: 86108
[startup+240.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 21478 0 0 0 23949 53 0 0 25 0 1 0 421738164 90275840 21259 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22040 21259 603 41 0 21999 0
vsize: 88160
[startup+250.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 21997 0 0 0 24948 54 0 0 25 0 1 0 421738164 92381184 21778 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22554 21778 603 41 0 22513 0
vsize: 90216
[startup+260.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 24130 0 0 0 25944 59 0 0 25 0 1 0 421738164 101122048 23911 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24688 23911 603 41 0 24647 0
vsize: 98752
[startup+270.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 26095 0 0 0 26940 63 0 0 25 0 1 0 421738164 109219840 25876 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26665 25876 603 41 0 26624 0
vsize: 106660
[startup+280.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 27238 0 0 0 27937 66 0 0 25 0 1 0 421738164 113831936 27019 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27791 27019 603 41 0 27750 0
vsize: 111164
[startup+290.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 29099 0 0 0 28933 70 0 0 25 0 1 0 421738164 121475072 28880 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29657 28880 603 41 0 29616 0
vsize: 118628
[startup+300.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 30340 0 0 0 29930 73 0 0 25 0 1 0 421738164 126636032 30121 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30917 30121 603 41 0 30876 0
vsize: 123668
[startup+310.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 31363 0 0 0 30928 75 0 0 25 0 1 0 421738164 130842624 31144 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31944 31144 603 41 0 31903 0
vsize: 127776
[startup+320.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 31788 0 0 0 31928 76 0 0 25 0 1 0 421738164 132259840 31520 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32290 31520 603 41 0 32249 0
vsize: 129160
[startup+330.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 31790 0 0 0 32928 76 0 0 25 0 1 0 421738164 132259840 31522 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32290 31522 603 41 0 32249 0
vsize: 129160
[startup+340.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 31791 0 0 0 33928 76 0 0 25 0 1 0 421738164 132259840 31523 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32290 31523 603 41 0 32249 0
vsize: 129160
[startup+350.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 31791 0 0 0 34928 76 0 0 25 0 1 0 421738164 132259840 31523 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32290 31523 603 41 0 32249 0
vsize: 129160
[startup+360.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 31793 0 0 0 35929 76 0 0 25 0 1 0 421738164 132259840 31525 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32290 31525 603 41 0 32249 0
vsize: 129160
[startup+370.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 31793 0 0 0 36929 76 0 0 25 0 1 0 421738164 132259840 31525 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32290 31525 603 41 0 32249 0
vsize: 129160
[startup+380.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 31793 0 0 0 37929 76 0 0 25 0 1 0 421738164 132259840 31525 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32290 31525 603 41 0 32249 0
vsize: 129160
[startup+390.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 31793 0 0 0 38929 76 0 0 25 0 1 0 421738164 132259840 31525 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32290 31525 603 41 0 32249 0
vsize: 129160
[startup+400.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 31793 0 0 0 39929 76 0 0 25 0 1 0 421738164 132259840 31525 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32290 31525 603 41 0 32249 0
vsize: 129160
[startup+410.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 31793 0 0 0 40930 76 0 0 25 0 1 0 421738164 132259840 31525 4294967295 134512640 134672761 3221224544 3221223584 134614191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32290 31525 603 41 0 32249 0
vsize: 129160
[startup+420.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 31793 0 0 0 41930 76 0 0 25 0 1 0 421738164 132259840 31525 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32290 31525 603 41 0 32249 0
vsize: 129160
[startup+430.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 31793 0 0 0 42930 76 0 0 25 0 1 0 421738164 132259840 31525 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32290 31525 603 41 0 32249 0
vsize: 129160
[startup+440.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 31793 0 0 0 43930 76 0 0 25 0 1 0 421738164 132259840 31525 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32290 31525 603 41 0 32249 0
vsize: 129160
[startup+450.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 31793 0 0 0 44930 76 0 0 25 0 1 0 421738164 132259840 31525 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32290 31525 603 41 0 32249 0
vsize: 129160
[startup+460.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 31793 0 0 0 45931 76 0 0 25 0 1 0 421738164 132259840 31525 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32290 31525 603 41 0 32249 0
vsize: 129160
[startup+470.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 31793 0 0 0 46931 76 0 0 25 0 1 0 421738164 132259840 31525 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32290 31525 603 41 0 32249 0
vsize: 129160
[startup+480.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 31793 0 0 0 47931 76 0 0 25 0 1 0 421738164 132259840 31525 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32290 31525 603 41 0 32249 0
vsize: 129160
[startup+490.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 31793 0 0 0 48931 76 0 0 25 0 1 0 421738164 132259840 31525 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32290 31525 603 41 0 32249 0
vsize: 129160
[startup+500.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 31793 0 0 0 49931 76 0 0 25 0 1 0 421738164 132259840 31525 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32290 31525 603 41 0 32249 0
vsize: 129160
[startup+510.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 31793 0 0 0 50931 76 0 0 25 0 1 0 421738164 132259840 31525 4294967295 134512640 134672761 3221224544 3221223356 1075350746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32290 31525 603 41 0 32249 0
vsize: 129160
[startup+520.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 31793 0 0 0 51932 76 0 0 25 0 1 0 421738164 132259840 31525 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32290 31525 603 41 0 32249 0
vsize: 129160
[startup+530.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 31793 0 0 0 52932 76 0 0 25 0 1 0 421738164 132259840 31525 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32290 31525 603 41 0 32249 0
vsize: 129160
[startup+540.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 31793 0 0 0 53932 76 0 0 25 0 1 0 421738164 132259840 31525 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32290 31525 603 41 0 32249 0
vsize: 129160
[startup+550.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 31793 0 0 0 54932 76 0 0 25 0 1 0 421738164 132259840 31525 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32290 31525 603 41 0 32249 0
vsize: 129160
[startup+560.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 31793 0 0 0 55932 76 0 0 25 0 1 0 421738164 132259840 31525 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32290 31525 603 41 0 32249 0
vsize: 129160
[startup+570.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 31793 0 0 0 56933 76 0 0 25 0 1 0 421738164 132259840 31525 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32290 31525 603 41 0 32249 0
vsize: 129160
[startup+580.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 31793 0 0 0 57933 76 0 0 25 0 1 0 421738164 132259840 31525 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32290 31525 603 41 0 32249 0
vsize: 129160
[startup+590.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 31793 0 0 0 58933 76 0 0 25 0 1 0 421738164 132259840 31525 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32290 31525 603 41 0 32249 0
vsize: 129160
[startup+600.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 31793 0 0 0 59933 76 0 0 25 0 1 0 421738164 132259840 31525 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32290 31525 603 41 0 32249 0
vsize: 129160
[startup+610.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 31793 0 0 0 60933 76 0 0 25 0 1 0 421738164 132259840 31525 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32290 31525 603 41 0 32249 0
vsize: 129160
[startup+620.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 31793 0 0 0 61933 76 0 0 25 0 1 0 421738164 132259840 31525 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32290 31525 603 41 0 32249 0
vsize: 129160
[startup+630.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 31794 0 0 0 62934 76 0 0 25 0 1 0 421738164 132259840 31526 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32290 31526 603 41 0 32249 0
vsize: 129160
[startup+640.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 31794 0 0 0 63934 76 0 0 25 0 1 0 421738164 132259840 31526 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32290 31526 603 41 0 32249 0
vsize: 129160
[startup+650.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 31795 0 0 0 64934 76 0 0 25 0 1 0 421738164 132259840 31527 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32290 31527 603 41 0 32249 0
vsize: 129160
[startup+660.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 31795 0 0 0 65934 76 0 0 25 0 1 0 421738164 132259840 31527 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32290 31527 603 41 0 32249 0
vsize: 129160
[startup+670.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 31890 0 0 0 66934 76 0 0 25 0 1 0 421738164 132653056 31622 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32386 31622 603 41 0 32345 0
vsize: 129544
[startup+680.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 32146 0 0 0 67933 77 0 0 25 0 1 0 421738164 133701632 31878 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32642 31878 603 41 0 32601 0
vsize: 130568
[startup+690.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 32852 0 0 0 68932 79 0 0 25 0 1 0 421738164 136720384 32584 4294967295 134512640 134672761 3221224544 3221223356 1075350045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33379 32584 603 41 0 33338 0
vsize: 133516
[startup+700.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 34757 0 0 0 69927 84 0 0 25 0 1 0 421738164 144502784 34489 4294967295 134512640 134672761 3221224544 3221222556 134645302 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35279 34489 603 41 0 35238 0
vsize: 141116
[startup+710.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 34757 0 0 0 70927 84 0 0 25 0 1 0 421738164 144240640 34431 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35215 34431 603 41 0 35174 0
vsize: 140860
[startup+720.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 34757 0 0 0 71927 84 0 0 25 0 1 0 421738164 144240640 34431 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35215 34431 603 41 0 35174 0
vsize: 140860
[startup+730.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 34757 0 0 0 72928 84 0 0 25 0 1 0 421738164 144240640 34431 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35215 34431 603 41 0 35174 0
vsize: 140860
[startup+740.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 34757 0 0 0 73928 84 0 0 25 0 1 0 421738164 144240640 34431 4294967295 134512640 134672761 3221224544 3221223584 134612927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35215 34431 603 41 0 35174 0
vsize: 140860
[startup+750.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 34757 0 0 0 74928 84 0 0 25 0 1 0 421738164 144240640 34431 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35215 34431 603 41 0 35174 0
vsize: 140860
[startup+760.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 34757 0 0 0 75928 84 0 0 25 0 1 0 421738164 144240640 34431 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35215 34431 603 41 0 35174 0
vsize: 140860
[startup+770.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 34757 0 0 0 76928 84 0 0 25 0 1 0 421738164 144240640 34431 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35215 34431 603 41 0 35174 0
vsize: 140860
[startup+780.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 34757 0 0 0 77929 84 0 0 25 0 1 0 421738164 144240640 34431 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35215 34431 603 41 0 35174 0
vsize: 140860
[startup+790.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 34757 0 0 0 78929 84 0 0 25 0 1 0 421738164 144240640 34431 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35215 34431 603 41 0 35174 0
vsize: 140860
[startup+800.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 34757 0 0 0 79929 84 0 0 25 0 1 0 421738164 144240640 34431 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35215 34431 603 41 0 35174 0
vsize: 140860
[startup+810.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 34757 0 0 0 80929 84 0 0 25 0 1 0 421738164 144240640 34431 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35215 34431 603 41 0 35174 0
vsize: 140860
[startup+820.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 34757 0 0 0 81929 84 0 0 25 0 1 0 421738164 144240640 34431 4294967295 134512640 134672761 3221224544 3221223584 134612606 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35215 34431 603 41 0 35174 0
vsize: 140860
[startup+830.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 34757 0 0 0 82929 84 0 0 25 0 1 0 421738164 144240640 34431 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35215 34431 603 41 0 35174 0
vsize: 140860
[startup+840.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 34757 0 0 0 83930 84 0 0 25 0 1 0 421738164 144240640 34431 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35215 34431 603 41 0 35174 0
vsize: 140860
[startup+850.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 34757 0 0 0 84930 84 0 0 25 0 1 0 421738164 144240640 34431 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35215 34431 603 41 0 35174 0
vsize: 140860
[startup+860.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 34757 0 0 0 85930 84 0 0 25 0 1 0 421738164 144240640 34431 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35215 34431 603 41 0 35174 0
vsize: 140860
[startup+870.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 34757 0 0 0 86930 84 0 0 25 0 1 0 421738164 144240640 34431 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35215 34431 603 41 0 35174 0
vsize: 140860
[startup+880.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 34757 0 0 0 87930 84 0 0 25 0 1 0 421738164 144240640 34431 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35215 34431 603 41 0 35174 0
vsize: 140860
[startup+890.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 34757 0 0 0 88931 84 0 0 25 0 1 0 421738164 144240640 34431 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35215 34431 603 41 0 35174 0
vsize: 140860
[startup+900.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 34757 0 0 0 89931 84 0 0 25 0 1 0 421738164 144240640 34431 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35215 34431 603 41 0 35174 0
vsize: 140860
[startup+910.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 34757 0 0 0 90931 84 0 0 25 0 1 0 421738164 144240640 34431 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35215 34431 603 41 0 35174 0
vsize: 140860
[startup+920.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 34757 0 0 0 91931 84 0 0 25 0 1 0 421738164 144240640 34431 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35215 34431 603 41 0 35174 0
vsize: 140860
[startup+930.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 34757 0 0 0 92932 84 0 0 25 0 1 0 421738164 144240640 34431 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35215 34431 603 41 0 35174 0
vsize: 140860
[startup+940.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 34757 0 0 0 93932 84 0 0 25 0 1 0 421738164 144240640 34431 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35215 34431 603 41 0 35174 0
vsize: 140860
[startup+950.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 34757 0 0 0 94932 84 0 0 25 0 1 0 421738164 144240640 34431 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35215 34431 603 41 0 35174 0
vsize: 140860
[startup+960.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 35199 0 0 0 95931 85 0 0 25 0 1 0 421738164 146116608 34873 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35673 34873 603 41 0 35632 0
vsize: 142692
[startup+970.031 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 35785 0 0 0 96930 86 0 0 25 0 1 0 421738164 148627456 35459 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36286 35459 603 41 0 36245 0
vsize: 145144
[startup+980.032 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 36269 0 0 0 97930 87 0 0 25 0 1 0 421738164 150605824 35943 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36769 35943 603 41 0 36728 0
vsize: 147076
[startup+990.031 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 36932 0 0 0 98928 89 0 0 25 0 1 0 421738164 153284608 36606 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37423 36606 603 41 0 37382 0
vsize: 149692
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 37512 0 0 0 99927 90 0 0 25 0 1 0 421738164 155652096 37186 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38001 37186 603 41 0 37960 0
vsize: 152004
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 38204 0 0 0 100926 91 0 0 25 0 1 0 421738164 158568448 37878 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38713 37878 603 41 0 38672 0
vsize: 154852
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 39181 0 0 0 101924 93 0 0 25 0 1 0 421738164 162545664 38855 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39684 38855 603 41 0 39643 0
vsize: 158736
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 40782 0 0 0 102920 97 0 0 25 0 1 0 421738164 169193472 40456 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41307 40456 603 41 0 41266 0
vsize: 165228
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 41971 0 0 0 103918 100 0 0 25 0 1 0 421738164 173948928 41645 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42468 41645 603 41 0 42427 0
vsize: 169872
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 42792 0 0 0 104916 102 0 0 25 0 1 0 421738164 177315840 42466 4294967295 134512640 134672761 3221224544 3221223600 134644269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43290 42466 603 41 0 43249 0
vsize: 173160
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 42793 0 0 0 105916 102 0 0 25 0 1 0 421738164 177053696 42406 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43226 42406 603 41 0 43185 0
vsize: 172904
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 42793 0 0 0 106916 102 0 0 25 0 1 0 421738164 177053696 42406 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43226 42406 603 41 0 43185 0
vsize: 172904
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 42796 0 0 0 107917 102 0 0 25 0 1 0 421738164 177053696 42409 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43226 42409 603 41 0 43185 0
vsize: 172904
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 42796 0 0 0 108917 102 0 0 25 0 1 0 421738164 177053696 42409 4294967295 134512640 134672761 3221224544 3221223696 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43226 42409 603 41 0 43185 0
vsize: 172904
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 42796 0 0 0 109917 102 0 0 25 0 1 0 421738164 177053696 42409 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43226 42409 603 41 0 43185 0
vsize: 172904
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 42796 0 0 0 110917 102 0 0 25 0 1 0 421738164 177053696 42409 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43226 42409 603 41 0 43185 0
vsize: 172904
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 42796 0 0 0 111917 102 0 0 25 0 1 0 421738164 177053696 42409 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43226 42409 603 41 0 43185 0
vsize: 172904
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 42796 0 0 0 112918 102 0 0 25 0 1 0 421738164 177053696 42409 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43226 42409 603 41 0 43185 0
vsize: 172904
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 42798 0 0 0 113918 102 0 0 25 0 1 0 421738164 177053696 42411 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43226 42411 603 41 0 43185 0
vsize: 172904
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 42798 0 0 0 114918 102 0 0 25 0 1 0 421738164 177053696 42411 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43226 42411 603 41 0 43185 0
vsize: 172904
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 42798 0 0 0 115918 102 0 0 25 0 1 0 421738164 177053696 42411 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43226 42411 603 41 0 43185 0
vsize: 172904
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 42798 0 0 0 116918 102 0 0 25 0 1 0 421738164 177053696 42411 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43226 42411 603 41 0 43185 0
vsize: 172904
[startup+1180.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 42799 0 0 0 117919 102 0 0 25 0 1 0 421738164 177053696 42412 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43226 42412 603 41 0 43185 0
vsize: 172904
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 42799 0 0 0 118919 102 0 0 25 0 1 0 421738164 177053696 42412 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43226 42412 603 41 0 43185 0
vsize: 172904
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10159
Raw data (stat): 10159 (minisat+) R 10158 5897 5896 0 -1 0 42799 0 0 0 119919 102 0 0 25 0 1 0 421738164 177053696 42412 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43226 42412 603 41 0 43185 0
vsize: 172904
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.12 s]
Raw data (loadavg): 1.00 0.97 0.91 1/54 10159
Raw data (stat): 10159 (minisat+) Z 10158 5897 5896 0 -1 12 42799 0 0 0 119919 110 0 0 25 0 1 0 421738164 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.12
CPU time (s): 1200.3
CPU user time (s): 1199.19
CPU system time (s): 1.10583
CPU usage (%): 100.015
Max. virtual memory (Kb): 173160
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####